Lambda the Ultimate

Wow, that page is full of awesome papers!

Oleg Kiselyov's Continuations Page

"Delimited Control in OCaml, Abstractly and Concretely" was mentioned on LtU here, but didn't receive much follow-up other than some concern about not citing prior work, and a very weak defense by me.

Speaking for myself, I don't know anyone who has delved into delimited continuations as deeply as Oleg Kiselyov and Chung-chieh ("Ken") Shan have. It would be interesting to hear the context for SPJ's comment. It's perhaps worth remembering that two years later, SPJ co-authored [Dybvig, Peyton Jones and Sabry (JFP 2007)] in which new monad transformers for delimited continuations are provided. As for "dynamic [delimited] continuations, I still don't know," several of Oleg and Chung-chieh's papers establish that the "static" and "dynamic" delimited continuation operators are macro-expressible in terms of each other, so there's actually no tension between them.

Finally, "Delimited Control in OCaml, Abstractly and Concretely" is a slightly unfortunate title, as it derives an API, scAPI, for describing/defining delimited continuations. That API has an implementation in OCaml, but also one in R5RS Scheme, demonstrating its validity in both typed and untyped settings.

So at this point I have the opposite reaction to SPJ's in 2005: I'm convinced delimited continuations are a good idea, and in fact I'd like to see a language in which they're considered foundational, e.g. dynamic scoping is implemented in terms of them, etc.

One problem with implementing effects as a reify/reflect pair on top of delimited continuations is speed. If you implement state with delimited continuations it's much slower than state implemented with native machine mutation. Unfortunately the latter doesn't work properly when you use multiple effects. For example if you use a piece of state inside a backtracking computation, you want the state modifications to be undone on backtracking. On the other hand if you use state in conjunction with dynamic binding (=~ the reader monad), this issue doesn't arise.

How can we get best of both worlds by using the native state when possible and less efficient simulated state when necessary?

One reason for my recent resurgence in interest in highly metacircular (implementations of) languages: it seems to me that we can do a lot more with partial evaluation than we currently are. Maybe a good partial evaluator could optimize a static delimited-continuation-based "mutation" implementation down to a (provably observationally equivalent) "real" mutation implementation.

From the date on the quote, it looks like something SPJ may have said during the workshop itself...