[Haskell-cafe] The mother of all functors/monads/categories

[Max Bolingbroke]

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
>              | Bind MonadSyn (String -> MonadSyn)
>              | 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
a state monad in here.

Now the meat:

\begin{code}
normalise :: MonadSyn -> MonadSyn
normalise m = go m Return
  where
    go :: MonadSyn -> (String -> MonadSyn) -> MonadSyn
    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}

What's really fun about this is that I pretty much transcribed the
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