Continuations

Previously, we saw how to translate a term with shift0 and reset into a term without them. Even if the source term doesn’t have shift0 or reset, this translation is interesting in its own right, called the continuation-passing style or CPS transform.

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

From the above rules we can derive the general rule for applications:

            𝒞⟦t1 t2⟧ = 𝒞⟦let x1 = t1 in let x2 = t2 in x1 x2⟧
                     = λk. 𝒞⟦t1⟧ (λx1. (λk'. 𝒞⟦t2⟧ (λx2. x1 x2 k')) k)
                     = λk. 𝒞⟦t1⟧ (λx1. 𝒞⟦t2⟧ (λx2. x1 x2 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 an operator exit that receives the final answer and does not return.

Examples

Here are some examples, where we selectively perform some β reductions (called “administrative” reductions) to make it more clear how CPS works:

           𝒞⟦0⟧ exit = (λk. k 0) exit
                     ⟶ exit 0
       𝒞⟦λx. x⟧ exit = (λk1. k1 (λx. λk2. k2 x)) exit
                     ⟶ exit (λx. λk2. k2 x)
   𝒞⟦(λx. x) 0⟧ exit = (λk1. (λk2. k2 (λx. λk3. k3 x)) (λx1. (λk4. k4 0) (λx2. x1 x2 k1))) exit
                     ⟶ (λk2. k2 (λx. λk3. k3 x)) (λx1. (λk4. k4 0) (λx2. x1 x2 exit))
                     ⟶ (λx1. (λk4. k4 0) (λx2. x1 x2 exit)) (λx. λk3. k3 x)
                     ⟶ (λk4. k4 0) (λx2. (λx. λk3. k3 x) x2 exit)
                     ⟶ (λx2. (λx. λk3. k3 x) x2 exit) 0
                     ⟶ (λx. λk3. k3 x) 0 exit

Intuitively, every function in the source term, which takes a single argument x, becomes a function that you can think of as taking two arguments, the original argument x, and a continuation k.

More examples without the administrative reductions shown step-by-step:

  𝒞⟦(λx. x) (λy. y) 0⟧ exit = (λx. λk1. k1 x) (λy. λk2. k2 y) (λx1. x1 0 exit)
𝒞⟦(λx. x) ((λy. y) 0)⟧ exit = (λy. λk1. k1 y) 0 (λx1. (λx. λk2. k2 x) x1 exit)

Exercise. Try converting these:

    𝒞⟦(λx. λy. y) 0⟧ exit =
𝒞⟦(λx. x x) (λy. y)⟧ exit =

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, function calls are applications. A tail call is when the redex is the entire term; a non-tail call is of the form E[t] where the context E is not [·] and the redex t is not a value.

When evaluating a term in CPS, every reduction is either of

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

where the redex is always the entire term. So the operational semantics for terms in CPS don’t need either congruence rules or evaluation contexts.

Practically, this means that an implementation of the semantics doesn’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 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.