Abrupt Changes of Control

Here we add call-with-current-continuation (callcc) to the definition of LAMBDA completed in Tutorial 1, and call the resulting language LAMBDA++. While doing so, we will learn how to define language constructs that abruptly change the execution control flow.

Take over the lambda.k definition from Lesson 8 in Part 1 of this Tutorial, which is the complete definition of the LAMBDA language, but without the comments.

callcc is a good example for studying the capabilities of a framework to support abrupt changes of control, because it is one of the most control-intensive language constructs known. Scheme is probably the first programming language that incorporated the callcc construct, although similar constructs have been recently included in many other languages in one form or another.

Here is a quick description: callcc e passes the remaining computation context, packaged as a function k, to e (which is expected to be a function); if during its evaluation e passes any value to k, then the current execution context is discarded and replaced by the one encoded by k and the value is passed to it; if e evaluates normally to some value v and passes nothing to k in the process, then v is returned as a result of callcc e and the execution continues normally. For example, we want the program callcc-jump.lambda:

(callcc (lambda k . ((k 5) + 2))) + 10

to evaluate to 15, not 17! Indeed, the computation context [] + 10 is passed to callcc's argument, which then sends it a 5, so the computation resumes to 5 + 10. On the other hand, the program callcc-not-jump.lambda

(callcc (lambda k . (5 + 2))) + 10

evaluates to 17.

If you like playing games, you can metaphorically think of callcc e as saving your game state in a file and passing it to your friend e. Then e can decide at some moment to drop everything she was doing, load your game and continue to play it from where you were.

The behavior of many popular control-changing constructs can be obtained using callcc. The program callcc-return.lambda shows, for example, how to obtain the behavior of a return statement, which exits the current execution context inside a function and returns a value to the caller's context:

letrec f x = callcc (lambda return . (
  f (if (x <= 0) then ((return 1) / 0) else 2)
in (f -3)

This should evaluate to 1, in spite of the recursive call to f and of the division by zero! Note that return is nothing but a variable name, but one which is bound to the current continuation at the beginning of the function execution. As soon as 1 is passed to return, the computation jumps back in time to where callcc was defined! Change -3 to 3 and the program will loop forever.

callcc is quite a powerful and beautiful language construct, although one which is admittedly hard to give semantics to in some frameworks. But not in K :) Here is the entire K syntax and semantics of callcc:

syntax Exp ::= "callcc" Exp  [strict]
syntax Val ::= cc(K)
rule <k> (callcc V:Val => V cc(K)) ~> K </k>
rule <k> cc(K) V ~> _ =>  V ~> K </k>

Let us first discuss the annotated syntax. We declared callcc strict, because its argument may not necessarily be a function yet, so it may need to be evaluated. As explained above, we need to encode the remaining computation somehow and pass it to callcc's argument. More specifically, since LAMBDA is call-by-value, we have to encode the remaining computation as a value. We do not want to simply subsort computations to Val, because there are computations which we do not want to be values. A simple solution to achieve our goal here is to introduce a new value construct, say cc (from current-continuation), which holds any computation.

Note that, inspired from SDF, K allows you to define the syntax of helping semantic operations, like cc, more compactly. Typically, we do not need a fancy syntax for such operators; all we need is a name, followed by open parenthesis, followed by a comma-separated list of arguments, followed by closed parenthesis. If this is the syntax that you want for a particular construct, then K allows you to drop all the quotes surrounding the terminals, as we did above for cc.

The semantic rules do exactly what the English semantics of callcc says. Note that here, unlike in our definition of LAMBDA in Tutorial 1, we had to mention the cell <k/> in our rules. This is because we need to make sure that we match the entire remaining computation, not only a fragment of it! For example, if we replace the two rules above with

rule (callcc V:Val => V cc(K)) ~> K
rule cc(K) V ~> _ =>  V ~> K

then we get a callcc which is allowed to non-deterministically pick a prefix of the remaining computation and pass it to its argument, and then when invoked within its argument, a non-deterministic prefix of the new computation is discarded and replaced by the saved one. Wow, that would be quite a language! Would you like to write programs in it? :)

Consequently, in K we can abruptly change the execution control flow of a program by simply changing the contents of the <k/> cell. This is one of the advantages of having an explicit representation of the execution context, like in K or in reduction semantics with evaluation contexts. Constructs like callcc are very hard and non-elegant to define in frameworks such as SOS, because those implicitly represent the execution context as proof context, and the latter cannot be easily changed.

Now that we know how to handle cells in configurations and use them in rules, in the next lesson we take a fresh look at LAMBDA and define it using an environment-based style, which avoids the complexity of substitution (e.g., having to deal with variable capture) and is closer in spirit to how functional languages are implemented.

Go to Lesson 2, LAMBDA++: Semantic (Non-Syntactic) Computation Items.

MOVIE (out of date) [6'28"]