`solve` returns the value of its body, if any

[sungshik]

Issues

Sometimes, solve returns a value. Sometimes, it doesn't.

1. The precise circumstances when a value is returned, don't seem to be documented.
2. When solve doesn't return a value, the types of solve (...) {...} reported by the compiler and the interpreter are different (value vs void).

Example 1

int f() {
    int x = 0;
    return solve (x) {
        x += x < 5 ? 1 : 0;
    }
}

In this example, solve returns the final value of x.

Example 2

int f() {
    int x = 0;
    return solve (x) {
        if (x < 5) x += 1;
    }
}

In this example, solve doesn't return a value.

• The compiler reports: "Return type int expected, found value"
• The interpreter reports: "Expected int, but got void"

Example 3

int f() {
    int x = 0;
    return solve (x) {
        if (x < 5) x += 1;
        123;
    }
}

In this example, solve returns 123.

[mahills]

Someone else may have more detailed comments, but this makes sense in terms of the expressions and types used. In example 1, when x stops changing, the final expression evaluated would essentially be x += 0 (since, at that point, the condition would be false). For expression 3, the final expression evaluated is 123. For example 2, this is the difference in the static vs dynamic type of the final result. In both cases, this will end with the condition failing when x == 5. The static type of this, since there is no else branch, is value, which is the result of computing the least upper bound in the type hierarchy of both void and int (since neither is substitutable for the other). The dynamic type of this is void since that is the result of "running" the missing else. I do agree that documenting this, or maybe adding a warning, would be a good idea, since the behavior could be unexpected. I'll tag @PaulKlint in case I missed something there.

[PaulKlint]

@sungshik thanks for raising this issue and @mahills thanks for your analysis. I completely agree with it.

The title "solve returns a value -- sometimes" is a bit misleading and should be paraphrased as " solve returns the value of its body, if any". But, nitpicking apart, this should be better documented.

What kind of warning do you have in mind @mahills ?

[mahills]

I'm not sure how doable it would be to add the warning I would like myself, which would be specifically to warn about situations where the result could be void -- the type checker is doing the right thing, but it may just be unexpected behavior. Unfortunately, I can think of lots of ways to make this hard to check (simplest example: and if/then/else that contains an if/then with no else, so you can't just check the last expression in the solve for an if with no else). This may actually be something that would be better for a linter, since you could create a syntactic check that would catch typical cases and the logic of the type checker would not need to be made more complex.

[sungshik]

@mahills: Thank you for clarifying!

@PaulKlint: Thank you for the title suggestion; that's more accurate indeed.