How does `eff` implement delimited control?

[re-xyr]

I am reading eff's source code and I saw that in the control operation, it throws a captured frame up to the handler to deal with, instead of resuming it in place. To me (who probably does not have enough context), this seems like extra indirection. What is the motivation for this design?

[lexi-lambda]

There are several subtleties here:

• First of all, we want to efficiently support both control and control0.

• In computations that repeatedly capture and resume the continuation, it’s inefficient to eagerly resume every chunk of the captured continuation every time. That would result in large amounts of memory being copied back and forth between the heap and the stack. Instead, eff restores continuation chunks lazily: once a continuation chunk has been captured, eff leaves it in the heap until it’s actually returned to. This means a portion of the stack may effectively be “compressed”—instead of having the continuation frames on the stack directly, there’s a pointer to a heap-allocated continuation containing the frames.

• Eventually, I want to implement something like Scheme’s dynamic-wind in eff, which means I can’t just use distinct PromptTag#s to capture the continuation all at once (since that would skip over any intermediate dynamic-wind frames).

• When implementing the above two things, eff must not leak stack space. It is critical that the strategy we use for unwinding and rewinding the continuation does not introduce any additional continuation frames that were not in the original program, as that would create problems for programs like this one:

  naturals :: Coroutine i Natural :< effs => Eff effs a
  naturals = go 0 where
    go n = yield n *> go (succ n)

  This definition of go is tail-recursive, so it should use constant stack space (all other things being equal), but this is pretty easy to mess up unless we are very, very careful.

These requirements inform the “calling convention” used by EVM when capturing and restoring the continuation. This is all intimately related to the following comment:

https://github.com/lexi-lambda/eff/blob/8c4df4bf54faf22456354be18095b14825be5e85/eff/src/Control/Effect/Internal.hs#L283-L286

I still need to write up the appropriate Note to explain the full subtleties, but I’ll try to give a brief, high-level explanation here:

• In order to implement our custom calling convention that supports dynamic-wind and lazy continuation restores, we need some way to communicate to enclosing handlers what they should do when control returns to them. This suggests that we should just have a type like this:

  data ReturnToHandler
    = ReturnNormal Any
    | ReturnAborting PromptId Any
    | ReturnCapturing (Capture Any)

  Then, when promptVM installs the prompt, it can do something like this:

  result <- prompt# (ReturnNormal <$> m)
  case result of
    ...

  But this does not work! The use of ReturnNormal <$> m grows the captured continuation every time promptVM is called, so it will leak stack space if handleVM is used in a tail-recursive loop.

• This means we have to somehow implement our calling convention without growing the continuation inside the use of prompt#. But we need to be able to distinguish normal returns from aborts/captures, since we need to apply the onReturn handler when a normal return occurs. RTS exceptions give us a way to do this. When promptVM installs the prompt, it adds a call to onReturn outside of the prompt, so that path will get taken if the computation returns normally.

• When there’s a non-normal return, we have to somehow skip that onReturn handler, since in those situations it must not be called. The easiest way to do that is to throw an exception, which will unwind over the onReturn stack frame and get caught by our handler, which can then do whatever special behavior we need to do.

Another way of putting this is that we’re effectively using RTS exceptions as a way to determine whether or not a use of prompt# returned normally or not without growing the captured continuation. This works because RTS exceptions are a first-class mechanism that allow a computation to signal a non-normal return. Yes, this is all outrageously subtle, but that is why it is so important that this stuff is abstracted away in a library, not exposed directly to the user: getting this stuff right is too hard to make it possible to accidentally get it wrong.

[re-xyr]

Thanks for the writeup! The point about tail calls is indeed very subtle and helps me understand why onReturn exists. I have some other (perhaps stupid) questions:

• What is the significance of dynamic-wind in an effect system like eff? I think I kind of understand this one:

  Having dynamic-wind is crucial for having non-scoped resumptions; otherwise we don't have a way to change the handler vector installed for the resumption. Plus, restoring state for each continuation call also requires dynamic-wind.

• What does "restore the continuation lazily" mean in this context, is it "calling the continuation out of control0#"? Apart from that, in both scenarios it seems like the continuation is called almost immediately (either directly in control0#, or called right away when it is thrown to the corresponding prompt).