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?
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
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
Next, we rewrite the definitions using
Kont, rearranging arguments as necessary.
It is now obvious how
S is manipulating reified continuation objects.
(aside) Note that
begin is the same as
(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.
Inlining the definitions, we obtain a first order stack-based evaluator!
This is essentially the inverse to the derivation given in .