Matthew Chan

← back

A correspondence between deep/shallow embeddings and CPS/first order evaluators

19 May 2019

From a conversation today on twitter:

@Iceland_jack: (original tweet)

Expressing continuations as rewrite rules

begin :: ([a] -> res) -> res
begin k = k []
push :: [a] -> a -> ([a] -> res) -> res
push as a k = k (a : as)
add :: Num a => [a] -> ([a] -> res) -> res
add (a:b:rest) k = k (b+a:rest)
end :: [a] -> a
end [a] = a
example1 = begin push 5 push 6 add end

@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).

{-# LANGUAGE GADTs #-}
type Kont a = [a] -> a

Next, we rewrite the definitions using Kont, rearranging arguments as necessary.

begin :: Kont a -> a
begin k = k []
-- push :: a -> Kont a -> [a] -> a
push :: a -> Kont a -> Kont a
push a k as = k (a : as)
-- add :: Num a => Kont a -> [a] -> a
add :: Num a => Kont a -> Kont a
add k (a:b:rest) = k (b+a:rest)
end :: Kont a
end [a] = a

It is now obvious how S is manipulating reified continuation objects.

(aside) Note that begin is the same as eval.

eval :: Kont a -> a
eval = begin

(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.

data Begin a where
  Begin :: Code a -> Begin a
data Code a where
  Push  :: a -> Code a -> Code a
  Add   :: Code a -> Code a
  End   :: Code a

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 => Begin a -> a
eval1 (Begin prog)   = begin  (eval1' prog)
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 => Begin a -> a
eval2 (Begin prog) = eval2' prog []
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].

References

  1. Danvy and Nielsen, Defunctionalization at work
  2. Bahr and Hutton, Calculating correct compilers