Explainer for unified stack-switching proposal #74
Conversation
Skeleton explainer document.
* [explainer branch] Update Explainer.md * Update Explainer.md
Use the tag results to constrain the result type of the target continuation rather than using the tag parameters.
Mostly a placeholder for now, but provides a bit of context.
Extend outline.
Simplify the explanation of the typing rules by abbreviating `C.types[$ct] = cont $ft; C.types[$ft] = [t1*] -> [t2*]` to just `C.types[$ct] = cont [t1*] -> [t2*]`. We can use an auxiliary function to implement the same abbreviation in the formal spec.
[explainer] Abbreviate away continuation function types
This came up as a point of ambiguity in a recent discussion, with the other possible design being trapping when the search finds a handler with the correct tag but incorrect event kind.
When looking up a type on the context, expand it (using `~~`) into the expected composite type instead of using equality (`=`). Also fix some places where equality should have been used when looking up tags. Add `func` to expanded function types.
- Refactor the rules for handlers out so they do not need to be repeated for both `resume` and `resume_throw`. - Fix the constraint on the tag type in `(on $e switch)` handlers to ensure the tag result type is equal to the continuation return type. The tag result type must be a subtype of the resume result type to ensure the switched-to continuation has a compatible type, and it must also be a supertype to ensure the return continuation has a correct type. If we wanted to provide more flexibility here, we could upper bound the switched-to continuation result type with the tag results and lower bound the return continuation result type with the tag parameters, but I can't think of any benefit to doing that. - Fix the constraint on the return continuation result type in `switch`. We know the switched-from continuation returns `t*`, so we must type it as returning a supertype of `t*`, not a subtype. - Fix some mismatched iteration bugs.
* Remove barrier again * Update TOC
* Update TOC
* Add encoding for `(on $t switch)`. Consequently, the encoding of `(on $t $h)` changes slightly in that we require a leading byte to indicate the shape of the `on`-clause.
Co-authored-by: Daniel Hillerström <daniel.hillerstrom@ed.ac.uk>
Co-authored-by: Daniel Hillerström <daniel.hillerstrom@ed.ac.uk>
Co-authored-by: KC Sivaramakrishnan <kc@kcsrk.info>
* Add the invoker's continuation type as a type annotation to `switch`.
|
|
||
| ### One-shot continuations | ||
|
|
||
| Continuations in the current proposal are single-shot (aka linear), |
There was a problem hiding this comment.
Do multi-shot continuations put a significantly larger burden on the implementation?
Is the current proposal suitable to be amended/complemented by a future proposal adding multi-shot continuations?
There was a problem hiding this comment.
Whether it is difficult to implement depends on the particular semantics for multi-shot continuations and the architectural constraints of the implementing engine.
I do not think there is anything in this proposal that prohibits the future addition of an instruction for simulating multi-shot continuations via cloning, e.g. cont.clone : [(ref null $ct)] -> [(ref $ct) (ref $ct)].
There was a problem hiding this comment.
Thanks for the response.
Yeah, so like this proposal generalizes the concept of exceptions to non-local control flow, the hypothetical future proposal may generalize the continuations to multi-shot.
There was a problem hiding this comment.
IMO, it is pretty unlikely that engine providers will support the extension to multi-shot continuations.
There appear to be two primary issues:
- No current 'language of interest' depends on multi-shot continuations.
- Wasm is typically embedded in other environments, and those environments are dominated by languages like C/C++/Rust. It seems unlikely that multi-shot continuations can be made compatible with those implementation languages.
The new explainer describes a unified proposal which combines the previous typed continuations (WasmFX) and bag-of-stacks (BoS) proposals into one.