From a conversation today on twitter:

@Iceland_jack: (original tweet)

Expressing continuations as rewrite rules

@themattchan: This illustrates the natural correspondence between cps/defunctionalisation and deep/shallow embeddings nicely!

@Iceland_jack: I think I understand but can you clarify using code?

Here’s how.

The code presented gives an encoding of a stack machine language, `S`

, embedding its operational semantics in the operational semantics of the host language, `H`

. The syntax of `S`

is shallowly embedded in `H`

. The semantics of `S`

is a higher order CPS encoding in `H`

.

Let’s first reformulate it a bit to make the structure clearer.

We give a type for continuations which takes a stack to a result (in the domain `a`

).

Next, we rewrite the definitions using `Kont`

, rearranging arguments as necessary.

```
-- add :: Num a => Kont a -> [a] -> a
add :: Num a => Kont a -> Kont a
add k (a:b:rest) = k (b+a:rest)
```

It is now obvious how `S`

is manipulating reified continuation objects.

(aside) Note that `begin`

is the same as `eval`

.

(end of aside)

Now we can derive a deep embedding of `S`

by defunctionalisation. The constructors we need in our defunctionalised representation correspond directly to our language constructs!

`Begin`

is somewhat of a special case, so we separate it from the rest of the operations.

Note the correspondence between the types of the shallow and deep embeddings.

The new evaluation function takes the deep embedding to the shallow embedding.

```
eval1' :: Num a => Code a -> Kont a
eval1' (Push a rest) = push a (eval1' rest)
eval1' (Add rest) = add (eval1' rest)
eval1' End = end
```

Inlining the definitions, we obtain a first order stack-based evaluator!

```
eval2' :: Num a => Code a -> [a] -> a
eval2' (Push a rest) stk = eval2' rest (a : stk)
eval2' (Add rest) (a:b:stk) = eval2' rest (a+b:stk)
eval2' End [res] = res
```

This is essentially the inverse to the derivation given in [2].