Delimited continuations

We’ve looked at several kinds of effects – state, exceptions, generators, and nondeterminism – and seen that we can translate them into pure lambda calculus, but the translation is a whole-program transformation, not a macro translation. Here, we introduce a single extension to the lambda calculus that does make it possible to macro-express these other effects.

Motivation

Take a look at some of the evaluation rules for exceptions, generators, and nondeterminism:

try F[error] with t2 ⟶ t2                               E-TryConErr
gen F[yield v] ⟶ inr {v, λz. gen F[unit]}               E-GenConYield
collect F[amb v1 v2] ⟶ collect F[v1] ++ collect F[v2]   E-CollectConAmb

All of them have a “delimiter” (try, gen, collect) and one or more kinds of expressions (error, yield, amb, etc.) that can be used inside the delimiter. All of them use a special kind of context (F[·]) that contains the rest of the computation within the delimiter. Ordinarily, reductions inside the delimiter look like

collect F[pred (succ v)] ⟶ collect F[v]                 E-PredSucc, E-Context

But the rules E-TryConErr, etc., all do something different: they use F[·] zero or two times and/or wrap F[·] inside something else.

Here, we want to invent a new control operator that makes F[·] into a function, called a continuation, so that the program can do whatever it wants with the continuation. It can call it zero or two times, or it can wrap it inside something else. Thus it will be able to macro-express exceptions, generators, and nondeterminism.

Syntax and semantics

We introduce two new keywords, shift0 and reset.

t ::= ...
      reset t
      shift0 t

E ::= ...
      reset E
      shift0 E

F ::= ...
      shift0 F

          reset v ⟶ v
reset F[shift0 v] ⟶ v (λx. reset F[x])

shift0 expects its argument to be a function, and it’s normally called like shift0 (λk. t). Let’s call t the body. The shift0 expression takes the rest of the computation inside the innermost reset and packages it into a continuation. Then the body is evaluated with k bound to the continuation.

A trivial use of shift0 is shift0 (λk. k true):

reset F[shift0 (λk. k true)] ⟶ (λk. k true) (λx. reset F[x])
                             ⟶ (λx. reset F[x]) true
                             ⟶ reset F[true]

So shift0 (λk. k true) is equivalent to true.

Simulating other effects

Exceptions

What does shift0 (λk. true) do?

reset F[shift0 (λk. true)] ⟶ (λk. true) (λx. reset F[x])
                           ⟶ true

This is similar to an exception. More generally, exceptions can be implemented like this:

try t1 with t2 ≡ case reset (inr t1) of
                     inl x ⇒ t2 x
                   | inr x ⇒ x
raise ≡ λe. shift0 (λk. inl e)

Recall that in the semantics of exceptions, try v1 with t2 ⟶ v1. Let’s see if our simulated exceptions do the same.

try v1 with t2
    ≡ case reset (inr v1) of inl x ⇒ t2 x | inr x ⇒ x
    ⟶ case inr v1 of inl x ⇒ t2 x | inr x ⇒ x
    ⟶ v1

In the semantics of exceptions, the reduction for handling an exception is try F[raise v11] with t2 ⟶ t2 v11.

try F[raise v11] with t2
    ≡ case reset (inr F[(λe. shift0 (λk. inl e)) v11]) of inl x ⇒ t2 x | inr x ⇒ x
    ⟶ case reset (inr F[shift0 (λk. inl v11)] of inl x ⇒ t2 x | inr x ⇒ x
    ⟶ case (λk. inl v11) (λx. reset (inr F[x])) of inl x ⇒ t2 x | inr x ⇒ x
    ⟶ case inl v11 of inl x ⇒ t2 x | inr x ⇒ x
    ⟶ t2 v11

Above, the body of the shift0 did not call k. If it did, then evaluation of the reset expression would resume right where it left off. This could be used to simulate resumable exceptions.

Generators

Instead of having the body of shift0 call k right away, it could return k. Then we could save k until much later and still be able to call k to resume evaluating the reset expression. This is similar to generators.

Generators can be simulated like this:

gen t ≡ reset (inl t)
yield ≡ λo. shift0 (λk. inr {o, k})

If t never yields, then the generator evaluates to something of the form inl v.

When t yields o, control exits the generator with value inr {o, k}. At any point, we can call k i to resume the generator, as if i were the value of the yield expression.

Nondeterminism

What does shift0 (λk. {k false, k true}) do?

reset F[shift0 (λk. {k false, k true})]
    ⟶ (λk. {k false, k true}) (λx. reset F[x])
    ⟶ {(λx. reset F[x]) false, (λx. reset F[x]) true}
    ⟶ {reset F[false], reset F[true]}

Calling the continuation twice evaluates the context F[·] twice with two different values for the hole. This is similar to nondeterminism.

More generally, you can call k multiple times to resume evaluation multiple times. Thus, nondeterminism can be implemented like this:

collect t ≡ reset [t]
      amb ≡ λx1. λx2. shift0 (λk. (k x1) ++ (k x2))

Calling amb x replaces the rest of the reset with a term that says, resume the reset once for each element of x. Each of those evaluates to a list, and those lists are concatenated together to produce a final answer.

collect F[v] ≡ reset [v]
             = [v]
             
collect F[amb v1 v2] ≡ reset (cons F[(λx. shift0 (λk. (k v1) ++ (k v2)))] nil)
                     ⟶ reset (cons F[shift0 (k v1) ++ (k v2))] nil)
                     ⟶ (λk. (k v1) ++ (k v2)) (λx. reset (cons F[x] nil))
                     ⟶ ((λx. reset (cons F[x] nil)) v1) ++ ((λx. reset (cons F[x] nil)) v2)
                     ⟶ (reset (cons F[v1] nil)) ++ (reset (cons F[v2] nil))
                     ≡ collect F[v1] ++ collect F[v2]

State

In the previous example, we saw that if you put something (e.g., ++) around a call to k, that thing ends up around the reset expression.

This is true no matter what the “something” is. For example, you can use shift0 to make a λs appear outside of the reset:

reset F[shift0 (λk. λs. k s)] 0
    ⟶ (λk. λs. k s) (λx. reset F[x]) 0
    ⟶ (λs. (λx. reset F[x]) s) 0
    ⟶ (λx. reset F[x]) 0
    ⟶ reset F[0]

So shift0 (λk. λs. k s) grabs the first term after the reset expression.

Similarly, you can make an extra argument appear to the right of the reset:

reset F[shift0 (λk. k unit 0)]
    ⟶ (λk. k unit 0) (λx. reset F[x])
    ⟶ (λx. reset F[x]) unit 0
    ⟶ reset F[unit] 0

So shift0 (λk. k unit s) makes s appear after the reset expression and evaluates to unit.

Putting these two tricks together, we can use the place to the right of reset as a mutable state.

init s in t ≡ reset (let x' = t in λs'. x') s
get ≡ shift0 (λk. λs. k s s)
set ≡ λs'. shift0 (λk. λs. k unit s')

init 0 in (set (succ get); get)
    ≡ reset (let x' = (set (succ shift0 (λk. λs. k s s)); get) in λs'. x') 0
    ⟶ (λk. λs. k s s) (λx. reset (let x' = (set (succ x); get) in λs'. x')) 0
    ⟶ (λs. (λx. reset (let x' = (set (succ x); get) in λs'. x')) s s) 0
    ⟶ (λx. reset (let x' = (set (succ x); get) in λs'. x')) 0 0
    ⟶ reset (let x' = (set (succ 0); get) in λs'. x') 0
    ≡ reset (let x' = ((λs'. shift0 (λk. λs. k unit s')) (succ 0); get) in λs'. x') 0
    ⟶ reset (let x' = (shift0 (λk. λs. k unit (succ 0)); get) in λs'. x') 0
    ⟶ (λk. λs. k unit (succ 0)) (λx. reset (let x' = (x; get) in λs'. x')) 0
    ⟶ (λs. (λx. reset (let x' = (x; get) in λs'. x')) unit (succ 0)) 0
    ⟶ λx. reset (let x' = (x; get) in λs'. x') unit (succ 0)
    ⟶ reset (let x' = (unit; get) in λs'. x') (succ 0)
    ⟶ reset (let x' = get in λs'. x') (succ 0)
    ⟶* reset (let x' = succ 0 in λs'. x') (succ 0)
    ⟶ reset (λs'. succ 0) (succ 0)
    ⟶ (λs'. succ 0) (succ 0)
    ⟶ succ 0

In pure λ-calculus

We can simulate reset/shift0 in pure λ-calculus using a whole-program transformation.

Let R be the type of a reset expression. Inside this expression, every Nat becomes a (Nat → R) → R. A Nat → R is a continuation, a function looking for a Nat, so a (Nat → R) → R takes a continuation of Nat → R and it returns an R.

If a term has no shifts, it just passes the value of the term to the continuation:

               𝒯⟦x⟧ = λk. k x
           𝒯⟦λx. t⟧ = λk. k (λx. 𝒯⟦t⟧)

Application is straightforward as always:

           𝒯⟦x1 x2⟧ = x1 x2

The translation of let is:

𝒯⟦let x = t1 in t2⟧ = λk. 𝒯⟦t1⟧ (λx. 𝒯⟦t2⟧ k)

Roughly speaking, the continuation of t1 is t2, and the continuation of t2 is the continuation of the let expression.

The above translation, which is called the continuation-passing transform and results in continuation-passing style, is highly important in its own right, and we will look at it more closely in the next page.

The translation of shift0 and reset is weirdly simple. A shift0 x (where x is a variable) becomes a function that takes a continuation, passes it to x, and returns whatever x returns.

        𝒯⟦shift0 x⟧ = λk. x k = x

The translation of reset should give the translation of t an empty continuation:

         𝒯⟦reset t⟧ = 𝒯⟦t⟧ (λx. 𝒯⟦x⟧)

References

Asai and Kiselyov, Introduction to Programming with Shift and Reset

Filinski, 1994. Representing Monads. In Proc. POPL.

Materzok and Biernacki, 2012. A Dynamic Interpretation of the CPS Hierarchy. In Proc. APLAS.