Continuations (graduate section only)

Previously, we saw how to translate a term with shift0 and reset into a term without them. This translation was, in part:

               𝒞⟦x⟧ = λk. k x
           𝒞⟦λx. t⟧ = λk. k (λx. 𝒯⟦t⟧)
           𝒞⟦x1 x2⟧ = x1 x2
𝒞⟦let x = t1 in t2⟧ = λk. 𝒯⟦t1⟧ (λx. 𝒯⟦t2⟧ k)

If the source term was pure to begin with, then the target term is said to be in continuation-passing style.

For the examples on this page, assume λ-calculus with built-in natural numbers (written in base 10) and built-in functions add and mul.

               𝒞⟦n⟧ = λk. k n   (n ∈ ℕ)

Let add' and mul' be the CPS translations of add and mul, respectively:

             𝒞⟦add⟧ = add'
             𝒞⟦mul⟧ = mul'

The conversion of add (mul 3 3) (mul 4 4) to CPS is tedious, but it works out to be:

𝒞⟦add (mul 3 3) (mul 4 4)⟧
    = λk. mul' 3 3 (λv1. mul' 4 4 (λv2. add' v1 v2 k))

The final continuation

The CPS transform turns every term into a function on continuations – even the whole term. So if we want to actually evaluate a term in CPS, we need to apply it to a continuation. What should it be?

One simple answer is λx. x, but to emphasize the “finality” of this continuation, let’s invent a pseudofunction exit that receives the final answer and does not return.

    (λk. mul' 3 3 (λv2. mul' 4 4 (λv3. add' v2 v3 k))) exit
⟶ mul' 3 3 (λv2. mul' 4 4 (λv3. add' v2 v3 exit))
⟶ (λv2. mul' 4 4 (λv3. add' v2 v3 exit)) 9
⟶ mul' 4 4 (λv3. add' 9 v3 exit)
⟶ (λv3. add' 9 v3 exit) 16
⟶ add' 9 16 exit
⟶ exit 25

Every call is a tail call

A tail call is when one function calls another function as the very last thing it does, so that they both have the same return value. Tail calls are important because they can be translated into gotos; in particular, writing recursive functions so that recursive function calls are tail calls is efficient because the recursion can be translated into a loop.

In the λ-calculus, a term t1 is in the tail position of term t2 if one of the following is true:

• t1 is in the tail position of t and t is in the tail position of t2
• t1 ≡ t2
• t2 ≡ λx. t1
• t2 ≡ if t0 then t1 else t3
• t2 ≡ if t0 then t3 else t1

The last three cases are exactly the places our semantics says we don’t evaluate inside, i.e., we don’t have rules E ::= λx. E, E ::= if v then E else t, or E ::= if v then t else E.

In the right-hand sides of the equations defining CPS, every application t1 t2 falls into one of these categories:

1. t1 is a continuation

2. t1 takes two arguments and t2 is the first one

3. t1 takes a continuation and t2 is a continuation

In CPS, cases (a) and (c) are always tail calls, that is, they always occur in the tail position of the entire term. Case (b) is not, but if we regard case (c) as merely partial application, then we can say: in CPS every full application is in the tail position of the entire term.

This restriction has several benefits.

• The operational semantics could be simplified. We don’t need evaluation contexts anymore, because the evaluation context is always just [·]. We do need an additional evaluation rule for β-reduction because of case (b) above:

  (λx. t1) v2 v3 ⟶ [x↦v2]t1 v3

  But the congruence rules and/or evaluation contexts can go away.

• In the corresponding implementation, we don’t need a stack. In your implementation of the big-step semantics, you probably used function calls to achieve the same effect as a stack; under the assumption that the term to be evaluated is in CPS, you would be able to write an interpreter or compiler that doesn’t use target-language function calls.

The type of continuations

What does the CPS transform do to types? Consider a term t with type T; for simplicity, assume that T is a base type. (Function types are more complicated because 𝒞 is recursively applied to the return type.) The CPS transform turns this into a function looking for the final continuation, which we’ve decided is exit.

Since exit does not return, its return type should (arguably) be the null type, or the type that contains no values, usually written ⊥ and pronounced “bottom”. So

exit : T → ⊥
𝒞⟦t⟧ : (T → ⊥) → ⊥

Since every call is a tail call, every continuation must have the same return type as the final continuation, so for every term of base type T, the CPS transform turns it into a term of type (T → ⊥) → ⊥, and its continuation has type T → ⊥.

Under the Curry-Howard isomorphism, ⊥ corresponds to false. And recall that X→Y in classical logic is defined to be ¬X ∨ Y. So the type of a continuation corresponds to T → ⊥ = ¬T ∨ false = ¬T. In other words, continuations correspond to negation.