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 `reset`

s and two `shift`

s. 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 `shift`

s, 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 these two 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))))
```