Rewriting Monadic Expressions with Template Haskell

The goal today is to implement an impossible Haskell function. But as this is a literate Haskell post we need to get some boilerplate out of the way:

> module Test where

> import Language.Haskell.TH
> import Control.Monad
> import Control.Monad.Reader
> import Control.Monad.Cont
> import IO

> infixl 1 #

So back to the impossible function: all monads m come equipped with a function of type a -> m a. But it's well known that you can't "extract elements back out of the monad" because there is no function of type m a -> a. So my goal today will be to write such a function. Clearly the first line of code ought to be:

> extract :: Monad m => m a -> a

The rest of the post will fill in the details.

The type declaration tells us what role it plays syntactically, ie. it tells us how we can write code with extract that type checks. But what should the semantics be?

For the IO monad an answer is easy to guess. 1 + extract (readLn :: IO Int) should execute readLn by reading n integer from stdin, strip of the IO part of the the return value and then add 1 to the result. In fact, Haskell already has a function that does exactly that, unsafePerformIO. The goal here is to implement extract in a way that works with any monad.

What might we expect the value of 1 + extract [1,2,3] to be? The value of extract [1,2,3] surely must be 1, 2 or 3. But which one? And what happens if the list is empty? There really isn't any way of answering this while remaining *purely* functional. But if we were running code on a suitable machine we could fork three threads returning one of 1, 2 and 3 in each thread, and then collecing th results together in a list. In other words, we'd expect the final result to be [2,3,4]. This would make extract a lot like McCarthy's ambiguous operator.

So it's clear that we can't interpret extract as a pure function. But we could try implementing it on a new abstract machine. But there's another approach we could take. A couple of times I've talked about a function of type ~~a -> a where ~a is the type a -> Void and Void is the type with no elements. This corresponds to double negation elimination in classical logic. The Curry-Howard isomorphism tells us no such function can be implemented in a pure functional language, but we can translate expressions containing references to such a function into expressions that are completely pure. This is the so-called CPS translation. Anyway, I had this idea that we could do something limilar with monads so that we could translate expressions containing extract into ordinary Haskell code. Turns out there's already a paper on how to do this: Representing Monads by Andrzej Filinski.

To translate all of Haskell this way would be a messy business. But just for fun I thought I'd implement a simpler translation for a small subset of Haskell. It's simply this:

For a choice of monad m denote the translation of both types and values by T. So x::a becomes T(x)::T(a). The translation is simply:

T(a) = m a on types
T(f x) = T(f) `ap` T(x)
T(extract x) = join T(x)

The important thing is that extract of type m a -> a is replaced by join of type m (m a) -> m a.

A great way to translate Haskell code is with Template Haskell. So here's some code:

> (#) x y = liftM2 AppE x y

> rewrite :: Exp -> ExpQ

> rewrite (AppE f x) = do
>     e <- [| extract |]
>     if f==e
>         then [| join |] # rewrite x
>         else [| ap |] # rewrite f # rewrite x

Most of the rest is support for some forms of syntactic sugar. First the infix operators:

> rewrite (InfixE (Just x) f Nothing) =
>     [| fmap |] # return f # rewrite x

> rewrite (InfixE (Just x) f (Just y)) =
>     [| liftM2 |] # return f # rewrite x # rewrite y

> rewrite (InfixE Nothing f (Just y)) =
>     [| fmap |] # ([| flip |] # return f) # rewrite y

And list operations. For example [a,b,c] is sugar for a : b : c : [].

> rewrite (ListE []) = [| return [] |]

> rewrite (ListE (x:xs)) =
>     [| liftM2 |] # [| (:) |] # rewrite x # rewrite (ListE xs)

> rewrite x =
>     [| return |] # return x

> test :: ExpQ -> ExpQ
> test = (>>= rewrite)

extract itself is just a placeholder that is supposd to be translated away:

> extract = undefined

If the above is placed in a file called Test.lhs then you can try compiling the following code.

{-# LANGUAGE TemplateHaskell #-}

import Test
import Control.Monad
import Control.Monad.Reader
import Control.Monad.Cont

ex1 = $(test [|
        extract [1,2] + extract [10,20]
    |])
ex2 = runReader $(test [|
        extract ask + 7
    |]) 10
ex3 = $(test [|
        1+extract (readLn :: IO Int)
    |] )

The big omission is the lack of translation for lambda abstractions. I think that to get this right might requires translating all of the code using -|extract|- from the ground up, not just isolated expressions like those above. And like with CPS, you lose referential transparency and the order in which expressions are evaluated makes a difference.

Anyway, this is a partial answer to the question posed here on "automonadization".