An Interpreter with Delimited Control Operators

In a previous post, I showed an interpreter written in continuation-passing style is able to support (unlimited) control operators such as call/cc. In this post, I extend that interpreter to support delimited controls: reset and shift. The taget language is a call-by-value lambda calculus with arithmetics.

The purpose of reset is to set a delimitation. The operator shift captures the current continuation (just like call/cc) but bounded with the nearest delimitation, and binds the delimited continuation to a name. But unlike unlimited continuations, delimited continuations return to its call-site instead of going through down to halt of computation.

Examples

For readers who don’t know shift and reset, I use step-by-step examples to demonstrate how they work.

Simple Example

Consider the following Scheme program:

{+ 5 {reset 
      {+ 2 
         {shift k 
                {+ 1 {k {k 3}}}}}}}

We set a boundary of continuation by reset, and then capture the continuation by shift and name it k. Conceptually, k is a function {lambda {v} {+ 2 v}}. Because of k is delimited, so the rest computateion {+ 5 ...} is not part of k.

The first application of k is {k 3}, so the value of this call-site would be {+ 3 2} which is 5. Then the program become:

{+ 5 {reset 
      {+ 2 
         {shift k 
                {+ 1 {k 5}}}}}}

Okay, now we have another application to k. Again, the expanded expression is { {l {v} {+ 2 v}} 5 } which is 7. By replacing 7 to its call site, we obtain:

{+ 5 {reset 
      {+ 2 
         {shift k 
                {+ 1 7}}}}}

Then {+ 1 7} is trivial:

{+ 5 {reset 
      {+ 2 
         {shift k 8}}}}

Because we don’t have any call to k, then the computation just transfers to {+ 5 ...}, and we can obtain the final value which is 13.

Equations for Reasoning

Before we step into the next example, I would like to introduce two equations for reasoning about reset/shift programs:

(reset val) = val
(reset E[(shift k expr)] = (reset ((lambda (k) expr)
                                   (lambda (v) (reset E[v]))))

The E in the second equation is the innermost evaluation context that not includes a reset. By applying these two equations inductively, we will obtain the program that can be evaluated as normally we do.

Complex Example

You may be confused about these equations, but we will see how to apply them in an example:

{+ 1 {reset {+ 2 {reset {+ 4 {shift k {shift k2 8}}}}}}}

The above program has two resets and two shifts. We first apply the second equation to the first shift, and identify the evaluation context as {+ 4 ...} (the computation between the most recent shift and this shift). So the program is transformed to:

{+ 1 {reset {+ 2 {reset {{lambda {k} {shift k2 8}}
                         {lambda {v} {reset {+ 4 v}}}}}}}}

Now we still have a shift expression {shift k2 8}. By continuing applying the second equation to it we may obtain:

{+ 1 {reset {+ 2 {reset {{lambda {k2} 8}
                         {lambda {v2}
                           {reset {{lambda {k} v2}
                                   {lambda {v} {reset {+ 4 v}}}}}}}}}}}

It is worth noting that the evaluation context E here is a function application:

{{lambda {k} ...} {lambda {v} {reset {+ 4 v}}}}

where the ... should be replace by the value that fills this evaluation context.

Now there is no shift in the program, and we can safely apply the function application or first equation. Since no where uses k2, so 8 just becomes the value of function applications:

{+ 1 {reset {+ 2 {reset 8}}}}

The first equation tells us reseting a value is just the value itself:

{+ 1 {reset {+ 2 8}}}

And the final value 11 can be easily obtained.

Another Complex Example

We can further change a little bit on previous example:

{+ 1 {reset {+ 2 {reset {+ 4 {shift k {shift k2 {k {k2 8}}}}}}}}}

The delimited continuations k and k2 is used inside. Note that shift also creates a boundary for other innert shifts, so the innert delimited continuation won’t exceed the outer shift. The transformation remain largely the same and the fully expanded code looks like this:

{+ 1 {reset {+ 2 {reset {{lambda {k2} {k2 8}}
                         {lambda {v2}
                           {reset {{lambda {k} {k v2}}
                                   {lambda {v} {reset {+ 4 v}}}}}}}}}}}

Danvy and Filinski’s paper Abstracting Control (1990) is also a great reference.

Implementation

To supprt the two delimited control operators, we modify a normal continuation-passing style interpreter. The infrastructures is used as normal: an associated list is used as data structure for environment; a binding is just a name and a value; lookup function just linearly traverses the environment. Two first-order data structure is used to represent closure and continuation: Closure and Cont, where Closure contains three compoenents and Cont just has a higher-order function as real continuation.

(define mt-env '())
(define ext-env cons)

(define bind (λ (name val) (cons name val)))
(define bind-name car)
(define bind-val cdr)

(define lookup
  (λ (x env)
    (cond [(null? env) (error 'lookup "free variable")]
          [(equal? x (bind-name (car env)))
           (bind-val (car env))]
          [else (lookup x (cdr env))])))

(struct Closure (arg body env))
(struct Cont (body))

To support delimited continuations, we introduce another formal argument meta-continuation r to the interpreter function (cps in this case). The types of cps, normal continuation normal-k and meta-continuation meta-k are showed as follows:

cps :: exp -> env -> normal-k -> meta-k -> ans
normal-k :: meta-k -> value -> ans
meta-k :: value -> ans

In principle, the type ans and value can be different, but in this case they are the same thing. The normal continuation takes two arguments, a meta-continuation and a value, then returns a value. A meta-continuation just takes a value and also returns a value.

Meta-Continuations

(define cps
  (λ (exp env k r)
    (match exp
      [(? number? x) ((k r) x)]
      [(? symbol? x) ((k r) (lookup x env))]
      [`(+ ,lhs ,rhs)
       (cps lhs env
            (λ (r)
              (λ (l-v)
                (cps rhs env
                     (λ (r)
                       (λ (r-v)
                         ((k r) (+ l-v r-v))))
                     r)))
            r)]
      [`(* ,lhs ,rhs)
       (cps lhs env
            (λ (r)
              (λ (l-v)
                (cps rhs env
                     (λ (r)
                       (λ (r-v)
                         ((k r) (* l-v r-v))))
                     r)))
            r)]
      [`(lambda (,x) ,body) ((k r) (Closure x body env))]
      [`(let (,name ,e) ,body)
       (cps `((lambda (,name) ,body) ,e) env k r)]
      [`(let/cc ,x ,body)
       (cps `(call/cc (lambda (,x) ,body)) env k r)]
      [`(call/cc (lambda (,x) ,body))
       (cps body (ext-env (bind x (Cont (λ (k1)
                                          (λ (r)
                                            (λ (v)
                                              ((k r) v)))))) ;; discard k1, do k and just escape
                          env)
            k
            r)]
      [`(reset ,e)
       (cps e env (λ (r) r) (k r))]
      [`(shift ,x ,e)
       (cps e (ext-env (bind x (Cont (λ (k1)
                                       (λ (r)
                                         (λ (v)
                                           ((k (k1 r)) v)))))) ;; do k first, then go back and do k1
                       env)
            (λ (r) r)
            r)]
      [`(,fun ,arg)
       (cps fun env
            (λ (r)
              (λ (fun-v)
                (cond [(Closure? fun-v)
                       (cps arg env
                            (λ (r)
                              (λ (arg-v)
                                (cps (Closure-body fun-v)
                                     (ext-env (bind (Closure-arg fun-v) arg-v)
                                              (Closure-env fun-v))
                                     k
                                     r)))
                            r)]
                      [(Cont? fun-v) (cps arg env ((Cont-body fun-v) k) r)]))) ;; feed with current continuation `k`
            r)])))

One way to think about meta-continuation is it is a continuation of continuation, or composition of continuations. As we can see, in the interpreter, the very common usages of k and r is (k r). For example, if the expression we are interpreting is a variable, what we do is ((k r) (lookup x env)), this can be interpreted as getting the corresponding value of variable x in the environment env, and use that value to the continuation, where the continuation is the composition of k and r. The actual value of k decides what should do according to the semantics.

Next, the real interesting things in the interpreter is how we handle reset call/cc and shift.

First of all, the value stored in Cont is a function with type normal-k -> meta-k -> value -> value. This is what we put into Cont when handling call/cc and shift. And when we dereference a continuation (the Cont case in function application), we accordingly feed the current continuation k to the continuation introduced by call/cc or shift (that is, (Cont-body fun-v)).

For reset and shift, the new normal continuation to the next call of cps is set to be an identity function (λ (r) r) which is so called to be delimited. But if a computation is finished to a reset, what should do next? Obviously we need a way to save the current continuation k and restore it sometime, that is by replacing meta-continuation to the composition (k r). This can be interpreted as do k first, and then do r. But note that call/cc do not change this part since it is not delimiting semantics.

In shift, we do not change the meta-continuation for the next recursive call to cps. Because if the shift is arounded by a reset then the meta-continuation is handled by reset; otherwise, the shift just shifts the control to the end of computation just like an unlimited continuation (e.g., (+ 1 (+ 2 (shift 3))) => 3).

Then we take a closer look at the continuation bindings created in call/cc and shift. They have the same type: normal-k -> meta-k -> value -> value but are still slightly different. k1 is the current continuation when invoking the captured continuation, and k is the continuation when creating this captured continuation. What call/cc does is, when invoking the captured continuation, the control is transferred to the continuation k (composed with r). But by invoking the continuation captured by shift, the control is transferred to the continuation k firstly, and then transferred back to k1, which is the local continuation when invoking it. This is the semantics that delimited continuation returns to its call site after reaching the delimitation.

Finally, for the purpose of evaluating a term, we define a function interp that uses default continuation and meta-continuation for cps.

(define interp
  (λ (e)
    (cps e mt-env (λ (r) (λ (v) (r v))) (λ (x) x))))