[Haskell-cafe] The mother of all functors/monads/categories
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
> | 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
More information about the Haskell-Cafe
mailing list