> 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".

## 5 comments:

Nice post, but you forgot

> {-# LANGUAGE TemplateHaskell #-}

as the first line of Test.lhs.

Can you elaborate on the comment that 1 + extract [1,2,3] -> [2,3,4] is like McCarthy's ambiguous operator? As I understood the latter, it is about backtracking.

Arnar,

Like amb in the sense that you can examine the value of

$(test [| extract [1,2,3]*extract [4,5,6]==8 |] )

to find out if 8 factors as a certain type of product, as in example.

Can someone explain to me why I get a parsing error on this line:

> (#) x y = liftM2 AppE x y

But this code is fine:

> x # y = liftM2 AppE x y

(# is the GHC syntax for an unboxed tuple. It's therefore magic, and you can't use it anywhere (making # a generally poor choice for an operator name, even though it's not reserved). You can get around it by writing ( # ) = ... instead.

Post a Comment