Supplementary Notes onContinuations15-312: Foundations of Programming LanguagesFrank PfenningLecture 10September 30, 2004In this lecture we first introduce exceptions [Ch. 13] and then continua-tions [Ch. 12], two advanced control construct available in some functionallanguages.Exceptions are a standard construct in ML and other languages such asJava. We give here only a particularly simple form; a more elaborate formis pursued in Assignment 4. It is particularly easy to describe now that ourabstract machines makes a control stack explicit.We introduce a new form of statek  failwhich signals that we are propagating an exception upwards in the con-trol stack k, looking for a handler or stopping at the empty stack. This“uncaught exception” is a particularly common form of implementing run-time errors. We do not distinguish different exceptions, only failure.We have two new forms of expressions fail1and try(e1, e2) (withconcrete syntax try e1ow e2). Informally, try(e1, e2) evaluates e1and re-turns its value. If the evaluation of e1fails, that is, an exception is raised,then we evaluate e2instead and returns its value (or propagate its excep-tion). These rules are formalized in the C-machine as follows.k > try(e1, e2) 7→ck . try( , e2) > e1k . try( , e2) < v17→ck < v1k > fail 7→ck  failk . f  fail 7→ck  fail for f 6= try( , )k . try( , e2)  fail 7→ck > e21A type should be included here in order to preserve the property that every well-typedexpression has a unique type, but we prefer not to complicate the syntax at this point.LECTURE NOTES SEPTEMBER 30, 2004L10.2 ContinuationsIn order to verify that these rules are sensible, we should prove appro-priate progress and preservation theorems. In order to do this, we need tointroduce some typing judgments for machine states and the new forms ofexpressions. First, expressions:Γ ` fail : τΓ ` e1: τ Γ ` e2: τΓ ` try(e1, e1) : τWe can now state (without proof) the preservation and progress prop-erties. The proofs follow previous patterns (see [Ch. 13]).1. (Preservation) If s : σ and s 7→ s0then s0: σ.2. (Progress) If s : σ then either(i) s 7→ s0for some s0, or(ii) s = • < v with v value, or(iii) s = •  fail.The manner in which the C-machine operates with respect to exceptionsmay seem a bit unrealistic, since the stack is unwound frame by frame.However, in languages like Java this is not an unusual implementationmethod. In ML, there is more frequently a second stack containing onlyhandlers for exceptions. The handler at the top of the stack is innermostand a fail expression can jump to it directly.Overall, such a machine should be equivalent to the specification ofexceptions above, but potentially more efficient. Often, we want to describeseveral aspects of execution behavior of a language constructs in severaldifferent machines, keeping the first as high-level as possible. However, wewill not pursue this further, but move on to the discussion of continuations.Continuations are more flexible, but also more dangerous than exceptions.Continuations are part of the definition of Scheme and are implementedas a library in Standard ML of New Jersey, even though they are not part ofthe definition of Standard ML. Continuations have been described as thegoto of functional languages, since they allow non-local transfer of control.While they are powerful, programs that exploit continuations can difficultto reason about and their gratuitous use should therefore be avoided.There are two basic constructs, given here with concrete and abstractsyntax. We ignore issues of type-checking in the concrete syntax.22See Assignment 4 for details on concrete syntax.LECTURE NOTES SEPTEMB ER 30, 2004Continuations L10.3callcc x => e callcc(x.e)throw e1to e2throw(e1, e2)In brief, callcc x => e captures the stack (= continuation) k in effect atthe time the callcc is executed and substitutes cont(k) for x in e. we canlater transfer control to k by throwing a value v to k with throw v to cont(k).Note that the stack k we capture can be returned past the point in which itwas in effect. As a result, throw can effect a kind of “time travel”. Whilethis can lead to programs that are very difficult to understand, it has multi-ple legitimate uses. One pattern of usage is as an alternative to exceptions,another is to implement co-routines or threads. Another use is to achievebacktracking.As a starting example we consider simple arithmetic expressions.(a) 1 + callcc x => 2 + (throw 3 to x) 7→∗c4(b) 1 + callcc x => 2 7→∗c3(c) 1 + callcc x => if (throw 2 to x) then 3 else 4 fi7→∗c3Example (a) shows an upward use of continuations similar to excep-tions, where the addition of 2 + is bypassed and discarded when wethrow to x.Example (b) illustrates that captured continuations need not be used inwhich case the normal control flow remains in effect.Example (c) demonstrates that a throw expression can occur anywhere;its type does not need to be tied to the type of the surrounding expres-sion. This is because a throw expression never returns normally—it al-ways passes control to its continuation argument.With this intuition we can describe the operational semantics, followedby the typing rules.k > callcc(x.e) 7→ck > {cont(k)/x}ek > throw(e1, e2) 7→ck . throw( , e2) > e1k . throw( , e2) < v17→ck . throw(v1, ) > e2k . throw(v1, ) < cont(k2) 7→ck2< v1k > cont(k0) 7→ck < cont(k0)The typing rules can be derived from the need to make sure both preser-vation and progress to hold. First, the constructs that can appear in thesource.LECTURE NOTES SEPTEMBER 30, 2004L10.4 ContinuationsΓ, x:τ cont ` e : τΓ ` callcc(x.e) : τΓ ` e1: τ1Γ ` e2: τ1contΓ ` throw(e1, e2) : τFinally, the rules for continuation values that can only arise during com-putation. They are needed to check the machine state, even though they arenot needed to type-check the input.k : τ ⇒ σΓ ` cont(k) : τ contIt looks like there could be a problem here, because σ, the final answertype of the continuation, does not appear in the conclusion. Fortunately, itworks, but only because the final answer type σ of all continuations thatmay occur in a computation will be equal. To be precise, if we want to betalk about typing intermediate states of the computation, we would needto pass along the final answer type σ through the typing judgments.As a more advanced example, consider the problem of composing afunction with a continuation. This can also be