Max Bolingbroke batterseapower at hotmail.com
Sun Jun 27 14:14:40 EDT 2010

On 27 June 2010 18:28, Max Bolingbroke <batterseapower at hotmail.com> wrote:
> I'm going to try automatically deriving a NBE algorithm for Moggi's
> monadic metalanguage from the Codensity monad - with luck it will
> correspond to the one-pass algorithm of Danvy.

Well, that works. On second thoughts, it's more akin to A-normalisation.

What I will show is how to derive an algorithm for A-normalisation
from the definition of the Codensity monad.

First, the language to normalise. Hacked this together, so I'm just
going to use Strings to represent terms of pure type:

> type Term = String

Terms of computational type:

> data MonadSyn = Return Term
>              | Foreign String

We have an injection from the pure terms, a bind operation in HOAS
style, and a "Foreign" constructor. I'm going to use Foreign to
introduce operations that have side effects but don't come from the
Monad type class. For example, we might include "get" and "put x" for

Now the meat:

\begin{code}
normalise m = go m Return
where
go (Return x)  k = k x
go (Bind m k)  c = go m (\a -> go (k a) c)

go (Foreign x) k = Bind (Foreign x) k
\end{code}

definition of the Codensity monad instance. The initial "Return" comes
from "lowerCodensity" and then I just typed in the Return and Bind
implementations pretty much verbatim:

>    return x = Codensity (\k -> k x)
>    m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

Foreign didn't come automatically: I had to use intelligence to tell
the normaliser how to deal with non-Monad computations. I'm happy with
that.

Now we can have an example:

\begin{code}
non_normalised = Bind (Return "10") $\x -> Bind (Bind (Bind (Foreign "get") (\y -> Return y)) (\z -> Bind (Foreign ("put " ++ x)) (\_ -> Return z)))$ \w ->
Return w

main = do
putStrLn "== Before"
print $pPrint non_normalised putStrLn "== After" print$ pPrint \$ normalise non_normalised
\end{code}

Which produces:

== Before
let x2 = 10
in let x0 = let x1 = let x4 = get
in x4
in let x3 = put x2
in x1
in x0
== After
let x2 = get
in let x0 = put 10
in x2

Amazing! A-normalisation of a monadic metalanguage, coming pretty much
mechanically from Codensity :-)

I'm going to try for normalisation of Lindleys idiom calculus now.

Cheers,
Max