Asymmetric coroutines without search

[tlively]

I'm definitely not proposing any changes to either proposed design, but I wanted to share this idea for discussion. I haven't talked with anyone about this yet.

Our discussion in #49 about how asymmetric coroutines are fundamentally more expressive than symmetric coroutines with respect to their interaction with JS got me thinking about how we could combine those benefits with the search-free switching ideas from the bag-o-stacks proposal. I know @slindley and others have emphasized in the past that it would be possible to change the design of typed continuations to avoid the need for handler search, but I haven't seen concrete details of what that could look like until now.

The main idea is that instead of a single stack type, we differentiate types for switching "up" the stack of stacks (i.e. suspending) and types for switching "down" the stack of stacks (i.e. resuming). Let's call the type for suspending prompt because we're switching up the stack to the prompt (i.e. handler, etc.) and the type for resuming cont because it is for resuming a delimited continuation.

comptype = ... | prompt t* (ref null? x) | cont t* (ref x)

C ⊢ prompt t1* (ref null? x) : ok
-- C.TYPES[x] = cont t2* rt

C ⊢ cont t1* (ref x) : ok
-- C.TYPES[x] = prompt t2* rt

Just like the stack type in bag-o-stacks, prompt and cont have a sequence of parameter types they expect to receive, where the last parameter must be a reference to where control just came from after a suspend or resume. For prompt, control must have just come from a cont and vice versa. The prompt reference parameter in a cont never needs to be nullable because the prompt will always exist immediately after a resume. In contrast, a cont may no longer exist if a continuation returns or retires to a prompt, so the cont reference in a prompt type may be nullable.

cont references can be created by cont.new, but there is no prompt.new. prompt references are only created by resume instructions.

C ⊢ cont.new x y : [] -> [(ref x)]
-- C.TYPES[x] = cont t1* (ref z)
-- C.FUNCS[y] = func t2* -> t3* rt
-- C.TYPES[z] = prompt t3* rt

The interesting thing here is that the results of the continuation function are identical to the values received by prompts the continuation will be able to suspend to. With this simple type system, prompts can only handle one kind of "event," i.e. one sequence of parameter types, so resume instructions do not need to be branch tables that can handle arbitrary different result types. By ensuring that the function results are the same as the prompt parameters, we avoid the need for a branch to differentiate suspends from normal returns, so resume does not need to branch at all. Of course producers can still differentiate suspends from normal returns in user space if they need to.

C ⊢ resume x : [t1* (ref null x)] -> [t2* rt]
-- C.TYPES[x] = cont t1* (ref y)
-- C.TYPES[y] = prompt t2* rt

The typing for suspend is very similar.

C ⊢ suspend x : [t1* (ref null x)] -> [t2* rt]
-- C.TYPES[x] = prompt t1* (ref null? y)
-- C.TYPES[y] = cont t2* rt

As an optimization, we can also allow continuations to retire themselves when they suspend, allowing their resources to be cleaned up eagerly. This is essentially non-local return up to a prompt.

C  ⊢ suspend_retire x : [t1* (ref null x)] -> [t2*]
-- C.TYPES[x] = prompt t1* (ref null y)

Note that the prompt type used with suspend_retire must have a nullable continuation reference parameter because it will receive a null value.

The last interesting instruction is suspend_switch, which is kind of like a tail-call for continuations. (This is called switch_to in the typed-continuations proposal). suspend_switch takes both a prompt reference and a cont reference. Control passes directly to the given continuation, which receives the given prompt reference as if it had been resumed from that prompt rather than from a sibling continuation. Since control does not actually pass to the prompt, the target continuation also needs to receive the reference to the previous continuation, otherwise there would be no live references to the previous continuation left after the switch.

C  ⊢ suspend_switch x : [t1* (ref null z) (ref null x)] -> [t2* rt]
-- C.TYPES[x] = cont t1* (ref null? y) (ref z)
-- C.TYPES[y] = cont t2* rt

Beyond these instructions, cont.new_ref, cont.bind, prompt.bind, and resume_throw would all be straightforward to include as well. suspend_switch_retire would also be possible, although it seems more niche.