WebAssembly / stack-switching

A repository for the stack switching proposal.
Other
146 stars 13 forks source link

Typed Continuations, resume, and type canonicalization #57

Closed titzer closed 6 months ago

titzer commented 6 months ago

In working through the typed continuations proposal, we noticed that the type rule for resume specifies that labels for handlers get not only the unpacked parameters to a tag, but also a new continuation ref on the stack. This continuation type is inferred from the result types of the tag. With Wasm GC having canonicalization of entire recursion groups, I'm not sure what to do with this rule (also, there is leftover structural subtyping on a function type here), as all rules for instructions should be using references to declared (and canonicalized) types so that their recursion group membership is explicit.

rossberg commented 6 months ago

The result types are determined by the labels, it is merely checked that the tags match these, but that check is after unrolling any recursion as usual, so should be fine.

titzer commented 6 months ago

Ah yes, I had realized that about an hour after posting this :). It's probably a minor thing that the rule is posed as having subtyping between function types, whereas it should probably be between vectors of parameter types and vectors of result types.

rossberg commented 6 months ago

Subtyping between function types is defined as you would expect. It is the same relation that is invoked when checking the validity of an explicit subtype declaration over function types.

titzer commented 6 months ago

Thanks.