Make br_if return the value of its value operand.

[sunfishcode]

This corresponds to WebAssembly/design#539.

[rossberg]

This doesn't look right, it breaks the implicit result dropping subsumption that is allowed for all other expressions. For example, you could no longer use a br_if with argument in a block, as your test cases already demonstrate:

(block (br_if $l (arg) (cond)) (other))

becomes a type error. That violates a basic design principle of the type system, and doesn't make sense from a practical perspective.

However, the previous version of this PR changed the typing of br and return. As @JSStats pointed out, it effectively reverted PR #180, which addressed issue #179. We could work around that with more special casing, but that would be fairly ugly, and I'm not convinced it's worth it.

I think the least inconsistent way to implement this change is to reach agreement that we undo #180. @jcbeyler, @lukewagner, would you be okay with that? It's not ideal either, but at this point, I don't have a particularly strong opinion about that one. It's still much better than introducing special case rules for optional arguments, which I'd very much like to avoid.

[sunfishcode]

From a purely practical perspective, there's no problem with making

    (block (br_if $l (arg) (cond)) (other))

a type error, because one can achieve a similar effect writing this code as

   (block (arg) (br_if $l (cond)) (other))

The practical restriction is that one can't use br_if to pass a value to one successor and drop it in the other. However, this restriction is consistent with how I expect to use br_if, and it's consistent with br_if's operand being strict. It's evaluated for both values of the condition, so it makes sense to type-check it for both values of the condition.

[lukewagner]

@rossberg-chromium Rather than revert, could we do br0/br0_if? That way we keep the syntactic arity match (which is what postorder needs) and then this PR would switch to check_type of an expr and the result-dropping works.

[rossberg]

@sunfishcode, that's not correct, the two expressions are completely different. The latter won't transfer arg to $l, and thus won't type-check if $l actually requires a value. There is no trivial way to rewrite the former under the current PR. You'll essentially need the encoding of a "drop" operator, avoiding which was a core design goal of the type system. (The simplest such encoding I can see would be (block (if (i32.const 1) (br_if $l (arg) (cond)) (other)).)

@lukewagner, special-casing typing on label arity would paint us into a corner regarding multiple values. I think we need a more future-proof solution. Reverting #180 is the one I can see.

I'm starting to wish we had a let-like construct, then we could easily desugar (br_if $l (arg) (cond)) as follows and get the desired typing for free:

(let $x (arg) (block (if (cond) (br $l (get_value $x))) (get_value $x)))

:)

[lukewagner]

@rossberg-chromium If we decoupled construction of tuples of values from br (such that you'd write (br_if $1 (tuple a b) (cond)) or just (br_if $1 (call foo_returning_tuple) (cond)), then is there a problem? In the model of this I have in my head, a tuple would just be 1 entry on the expr stack (so that means each entry on the expr stack is a Vector<Pair<Def,Type>> where Def is your compiler SSA definition) so you still want the binary br0/br split.

[lukewagner]

By any lucky chance are you so inclined to write such a PR :) ?

[ghost]

@rossberg-chromium Re: stack machine: yes, there are certainly CL implementations that are stack machines and these support multiple value expressions, but they keep a count of values on the stack at some points or a frame pointer as a reference position, but I think you are right that wasm would not need to do this because the runtime compiler always knows the number of actual and expected values at compile time, so even if wasm allows a mismatch between expected values of br_if consumers it would still know to pop any unused values. The only remaining concern might be if people expected to execute the AST literally as a byte code and then might need to keep track of the number of expression values at runtime (as opposed to the runtime compiler which can account for them at compile time).

I notice that if desugars to if_else in the ml-proto and that it can return a different number of values depending on the condition, and it might need to be the responsibility of the operators to return a consistent number of values here so if would want to return the empty-values irrespective of condition. Also if_else and selection might want to be defined to return a consistent number of values irrespective of the condition.

[rossberg]

@JSStats, under the tuple interpretation used in ml-proto's eval, it is neither necessary nor desirable to do that. Only a stack machine would require adjustments. But the approach you suggest would be the wrong one. Instead, you'd need to pop off the stack whenever the type system uses subsumption (i.e., "forgets" a non-empty value in check_type). That occurs in more places than just branches, e.g. (block (i32.const 0) (i32.const 1)) requires dropping the first value. Branches do not need any special treatment.

[ghost]

@rossberg-chromium Sorry, it's not clear to me what you are referring to as 'neither necessary nor desirable to do that'. As I understand your position, the 'tuple' proposal, it would only be possible to either discard the entire tuple or consume all the values, whereas for my 'values' proposal it would be possible to consume any length head of the values which includes both none and all as limiting cases and thus subsumes your tuple proposal and I believe can be demonstrate to be practically more useful and efficiently at encoding the lowered wasm for at least some languages. I believe these two proposals can be judged on their efficiency at encoding lowered code, and that a 'right' or 'wrong' subjective judgement is not necessary, and perhaps we could stop using such words and I apologise if I have framed some aspects of this issue in those terms.

In any case I still fail to see how tracking the number of values can be avoided. As noted, the runtime compiler seems to know the number of values at compile time so can optimize away tracking the number of values, but I fail to see how an interpreter of the literal AST could avoid tracking the number of values, be it the number of values in a tuple or the number of values in a values list? Even if the interpreter boxed the tuple, the tuple object would be encoding the number of values. Sorry if I am missing some obvious optimization that the tuple strategy supports, but perhaps you could share this if there is one?

I certainly agree that accounting for differences between the number of expected and actual values is a general operation and not specific to branches, and I just gave this as an example because this is the topic of this issue. However bf_if does seem to be a unique operation in wasm as it is the only operation that has multiple consumers of its result values and this might make it uniquely useful for discussing some aspects of the type system. Every other case of multiple references seems to go through variables. I support each consumer being handled separately for br_if so that one consumer can drop the values and the other consume them, and for the reason that this is more flexible and can thus increase the efficiency of coding some patterns.

[rossberg]

@JSStats, you are now talking about a language extension again, I wasn't. But even with more general subtyping like you propose, you wouldn't need or want to adjust tuples in the operational semantics. In a tuple-based implementation, subtyping just works, without coercing, because there is no operation that can ever observe excess values. They just get ignored when decomposing a tuple. A real-world implementation might of course want to implement that differently, e.g. a stack-based one has to.

[sunfishcode]

Closing this for now, so we can work out the multiple result design first.