2006-11-01 – Constraining continuations

So last week I wrote about some simple "desugaring" transformations that turn a fairly conventional block-structured programming language into the call-by-value lambda calculus with some small extensions. The main problem is that I relied on first-class continuations. This has at least two undesirable consequences:

Fortunately there's a nice solution: multi-return function calls. The idea is to separate continuation arguments from normal arguments, and restrict the continuations so that activation frames are still used in a normal stack-like LIFO manner. What's really neat is that it preserves a lot of the the power of first-class continuations.

However, the desugaring transforms become more complicated. The scope of the multi-return continuations is restricted so that you cannot (for example) return from a function by invoking its continuation from an inner block, because the continuation is not available there. Instead you have to add plumbing to pass the early-return continuation into the block along with the block's normal sequential continuation. This plumbing ends up being rather like the standard continuation-passing-style transformation described in the lambda-the-ultimate papers linked to above, but with an extra continuation for each early exit.

This extra-continuation plumbing is also similar to a standard implementation technique for exceptions (which I called "non-trivial" last week, but isn't actually hard to understand). As well as the sequential continuation that is passed around in CPS, you pass around an exception handler continuation which is invoked in order to throw an exception. This is very similar to implementing exceptions in C with setjmp and longjmp, except in C you can keep the current exception handler in a global variable instead of passing it around.

The downside of these techniques is that the plumbing is an overhead. However, it is "pay-as-you-go", in that you only need the plumbing if you use early exits from blocks. (It's less easy to avoid the exception plumbing since exceptions can usually be thrown anywhere.) By contrast, the more complicated infrastructure needed for first-class continuations affects the performance of the whole run-time system.

(The mathematics in the typing of these constructions relates directly to their balance of practicality and power. Constrained continuations like multi-return functions and exceptions are usually used linearly and have an intuitionistic (constructive) typing. Call-with-current-continuation, however, has a classical typing which is not expressible in most practical type systems. This kind of direct relationship between theory and practice is one of the beauties of computer science.)

⇐ 2006-10-27 ⇐ Job: head of networks and telecoms ⇐ ⇒ More log-structured MTA queues. ⇒ 2006-11-01 ⇒