https://parametri.city/blog/2019-05-19-cps-and-embeddings.html

cps1.lhs

@Iceland_jack: https://twitter.com/Iceland_jack/status/1130243968820830208

< 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: How?

----

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](https://www.brics.dk/RS/01/23/BRICS-RS-01-23.pdf)
2. [Bahr and Hutton, Calculating correct compilers](http://www.cs.nott.ac.uk/~pszgmh/ccc.pdf)