[Haskellcafe] Re: what is inverse of mzero and return?
Ross Paterson
ross at soi.city.ac.uk
Tue Jan 25 07:16:56 EST 2005
On Mon, Jan 24, 2005 at 09:23:29PM +0100, Daniel Fischer wrote:
 We face a severe problem here, not only that IO a is not an instance of Eq,
 which takes this whole discussion outside the realm of Haskell, on top of that
 we find the horrible fact that x /= x may be true in the IO Monad, consider

 x = getLine >>= putStrLn

 or anything similar  actually we already have getChar /= getChar
 and that holds whether we just consider the values returned by an IO
 action or take the action performed into account.
Eq is a bit of a red herring: function types don't belong to it either,
and yet we can still prove that two functions are equal. IO t is an
abstract type, but it can still be thought of as having values (distinct
from the values of type t, of course).
Suppose we take a concrete IO type (simplified by omitting exceptions):
> import Prelude hiding (IO, putChar, getChar)
> import qualified Prelude
> import Control.Monad
> type IO = Resumption SysCall
> data Resumption f a
> = Return a
>  Resume (f (Resumption f a))
> data SysCall a
> = GetChar (Char > a)
>  PutChar Char a
This encodes the idea that an IO computation either returns a value or
some instruction to the system, with a continuation to be entered after
the corresponding operation has been run.
We can define a monad instance for this type:
> instance Functor f => Monad (Resumption f) where
> return = Return
> Return v >>= f = f v
> Resume c >>= f = Resume (fmap (>>= f) c)
> instance Functor SysCall where
> fmap f (GetChar k) = GetChar (f . k)
> fmap f (PutChar c a) = PutChar c (f a)
and we can define the familiar operations:
> getChar :: IO Char
> getChar = Resume (GetChar Return)
> putChar :: Char > IO ()
> putChar c = Resume (PutChar c (Return ()))
and you can write programs as before, except that now they construct
values of the concrete IO type. Because the type is concrete, you can
say whether or not two values of type IO t are equal (even though it's
not in Eq either).
But how do you do anything with values of the madeup IO type? With the
builtin IO type, we say the external system grabs the result of main
and does something mysterious with it. We can do that with this type
too, except that the first part of the execution of the action is to
transform the concrete type into the builtin IO type:
> toIO :: IO a > Prelude.IO a
> toIO (Return a) = return a
> toIO (Resume c) = doSysCall c >>= toIO
> doSysCall :: SysCall a > Prelude.IO a
> doSysCall (GetChar k) = do
> c < Prelude.getChar
> return (k c)
> doSysCall (PutChar c m) = do
> Prelude.putChar c
> return m
Now one can prove that toIO is a monad transformation that preserves
the primitives (ignoring some pesky liftings of types):
toIO (return x) = return x
toIO (a >>= f) = toIO a >>= (toIO . f)
toIO getChar = Prelude.getChar
toIO (putChar c) = Prelude.putChar c
For example, here's the proof for getChar:
toIO getChar
= { definition of getChar }
toIO (Resume (GetChar Return))
= { definition of toIO }
doSysCall (GetChar Return) >>= toIO
= { definition of doSysCall }
(Prelude.getChar >>= \c > return (Return c)) >>= toIO
= { monad associativity law }
Prelude.getChar >>= (\c > return (Return c) >>= toIO)
= { monad left identity law }
Prelude.getChar >>= \c > toIO (Return c)
= { definition of toIO }
Prelude.getChar >>= \c > return c
= { monad right identity law }
Prelude.getChar
so we can push toIO all the way down the program we wrote, and any
equation we can prove between values of the concrete type becomes
an equation between values of the builtin one. There may be other
equations one could postulate for the abstract type, but they require
operational reasoning about the effect of operations on the system 
they're external to Haskell.
To talk about mzero and mplus, we'd need to extend the concrete IO type
with exceptions, but that's not too hard.
More information about the HaskellCafe
mailing list