Control flow operators type checking

[naturaltransformation]

Returns are desugared into brs, which may yield a value, before type checking, but the design docs require that return not yield a value https://github.com/WebAssembly/design/blob/master/AstSemantics.md#yielding-values-from-control-constructs. This behavior is used in certain test cases. Is this seeming discrepancy resolved somehow? Thanks!

[rossberg]

I'm not sure I understand. A br does not yield a value either. Can you give an example?

[naturaltransformation]

For example, in labels.wast's misc2 function the body type checks (i32.xor (return (i32.const 1)) (i32.const 2)). Also, (func (result i32) (if (i32.const 1) (return (i32.const 0)) (return (i32.const 1)))) type checks.

[rossberg]

Yes. But this is intentional: any operator that unconditionally transfers control is fully polymorphic, in order to e.g. allow it in branches whose siblings do yield some value. Same as in all other typed (expression) languages.

The design doc's formulation that something does "not yield a value" may be a bit misleading: it is only meant to describe the operational semantics, not typing.

[rossberg]

What's surprising about your second example, btw?

[naturaltransformation]

Ah! Thank you! Oh, no, the second example isn't surprising by itself, just surprising in the context of interpreting the design docs clause as imposing a static semantics. That is very helpful. It would be great to clarify that in the design docs. I can take a pass at doing that if it doesn't get in anyone's way.

[naturaltransformation]

Since there is no section or document in the design docs that describes the type system, would it be fair to say that the spec is (already) definitive in this matter?

[rossberg]

Yes, pretty much. Spelling out all details of a type system in prose isn't very compelling anyway.