(Delimited) continuations

[byorgey]

With CEK machines, it is extremely easy to add callcc and throw, so we might as well. Perhaps this capability should be provided by some kind of time machine device (ingredients: clock, phone booth, ...?)

Concretely:

• Add a new type: if t is a type, cont t is the type of continuations expecting a value of type t.
• Add constants callcc : forall t. (cont t -> t) -> t and throw : forall t1 t2. t1 -> cont t1 -> t2.
• To evaluate callcc, just package up the current continuation in the CEK machine and pass it to the function (i.e. push an FApp frame and produce the current continuation as a value).
• To evaluate throw v k, produce the output v but replace the current continuation with k.

[polux]

https://www.brics.dk/RS/06/15/BRICS-RS-06-15.pdf also describes a tweaked version of the CEK machine that supports delimited continuations, which would be even more fun :)

[polux]

In #150 @byorgey wrote:

how does having a CESK machine interact with continuations?

I don't know of a language where the continuation would capture the store. I may be fun though :) The closest thing I can think of is rollbacking a DB or STM transaction. As long as the store is only used for memoization and recursion we don't really need to ask ourselves this question though, semantics-wise.

[byorgey]

As long as the store is only used for memoization and recursion we don't really need to ask ourselves this question though, semantics-wise.

Right, agreed. But I think we are going to want mutable arrays (#98). I can't imagine naive implementations of continuations + mutable arrays would play nicely together at all. We could perhaps make continuations capture the store, as you mentioned, but this would rely on stores being persistent (e.g. we could not use actual IORefs as discussed in #150 ). One might also imagine some sort of system for recording, rolling back, and replaying changes to the store, DB transaction-style, when using continuations to jump around in time, but that seems complicated. Another possibility is some kind of type analysis to disallow unsafe combinations of features. PFPL Chapter 34 has a discussion of so-called "mobile" types that has to do with ruling out unsafe uses of references, but I don't yet understand it well enough to know if it is relevant/helpful.

[polux]

As written on IRC and as I wrote above, I think it is standard to not capture the store in continuations. So I can imagine a naive implementation of continuations + mutable arrays: this is what you get in scheme for instance. Whether or not it is nice is a matter of taste I guess :) But note that there are certain things that you cannot do if the store is rolled back everytime you restore a continuation. Implementing an early break from a loop that modifies an array for instance.

[byorgey]

Implementing an early break from a loop that modifies an array for instance.

Ah, good point. Yeah, maybe you're right, and there's not really an issue here. If you want to use continuations and mutable arrays you just have to be careful / know what you're doing.

[byorgey]

https://okmij.org/ftp/continuations/against-callcc.html argues against call/cc as a language primitive, which seems convincing. Maybe delimited continuations are indeed the way to go.

[byorgey]

It seems there are many different sets of control operators one can have for working with delimited continuations, but shift/reset seems the simplest and most standard? https://okmij.org/ftp/continuations/index.html#tutorial is a relevant tutorial.

https://brics.dk/RS/03/41/BRICS-RS-03-41.pdf seems like a simpler / more directly relevant reference for implementing shift + reset in a CE(S)K machine context.

[byorgey]

I really want the device providing continuations to be a time machine. More thoughts on a potential recipe tree:

• clock
  • quartz
  • 32 iron gears
  • glass
• 256 solar panels (a time machine requires a lot of power!)
• a bunch (16? 32? 64?) of circuits
• phone booth
  • 32 boards
  • some other silly things?

[byorgey]

So the essential idea of how to update the CESK machine to support delimited continuations is just to store, instead of a single continuation, a stack of continuations (though this is perhaps a bit confusing since we must remember that a continuation is itself represented as a stack of frames). Most of the time, things interact with the continuation on the top of the stack just as they did when we had a single continuation. But:

• To evaluate reset t, we focus on evaluating t with a new empty continuation pushed on top of the continuation stack.
• To evaluate shift k. t, we focus on evaluating t, with a new binding k -> C in the environment, where C is the current continuation; and that current continuation is replaced by an empty continuation on top of the continuation stack.
  • Question: are there good reasons for making shift a primitive binding form, or could we just have it take a lambda as an argument, shift (\k. t)?
  • I think we can just do the latter.
    • It would have type something like shift : (cont a -> b) -> b.
    • To evaluate shift (\k.t) we would evaluate (\k. t) C and let the rules for lambda take care of extending the environment etc.
• If the continuation on top of the stack ever becomes empty, we pop it off and proceed with the next one on the stack.

Many of the formulations I have seen have the "current continuation" as a separate thing from the stack, rather than always talking about the current continuation as the one on the top of the stack. That may or may not be a nicer way to organize things in practice.

[byorgey]

Note that typechecking shift and reset is a bit more complicated than I thought. Just having shift and reset by themselves with the types I mentioned above is obviously wrong, since there would be no way to use the special cont a value. So there would need to be some kind of built-in runCont or something like that. Also, cont needs two type parameters: one to represent the result type of the computation, and one to represent the eventual result type of the continuation (the "answer type"). We can model it after https://hackage.haskell.org/package/transformers-0.6.0.4/docs/Control-Monad-Trans-Cont.html , maybe? I am still not sure to what extent we would need to modify/enhance the type system to be able to have "native" delimited continuations. Haskell doesn't: you can only use shift/reset in the context of a Cont r a computation.

https://plv.mpi-sws.org/plerg/papers/danvy-filinski-89-2up.pdf is an example of a type system for a language with shift/reset. Indeed, it requires modifying the entire system to track additional type information.

[byorgey]

To summarize so far:

• Adding callcc and throw would be pretty easy: they are not hard to typecheck, and implementing them is really easy with a CESK machine.
• However, callcc and throw are not "cool".
• Delimited continuations are much nicer/cooler, but:
  • They are a bit harder to implement (we need a stack of continuations instead of just a continuation)
  • Doing static typechecking for them would require major changes to the type system.

The reason normal, undelimited continuations are easy to typecheck whereas delimited continuations are hard, seems to have to do with the fact undelimited continuations always have global scope, so we only have to keep track of the type they expect to be given; we don't need to keep track of any "answer type". Whereas with delimited continuations, we have to ensure that the type resulting from running a continuation matches up with its context, so every continuation is indexed by two types, and while typechecking we have to e.g. keep track of the type at the nearest enclosing reset.

Given all this I think we should go back to just implementing undelimited continuations, or don't add them at all.

[byorgey]

If we implement undelimited continuations, we have to be careful that using them can't screw up things like FRestoreEnv frames etc. Like you wouldn't want to use continuations and have it accidentally blow away all your in-scope definitions. It might all "just work" but we just want to be careful/thoughtful about it.