[Haskell-cafe] Re: what is inverse of mzero and return?

[Ross Paterson]

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 made-up IO type?  With the
built-in 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 built-in 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 built-in 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.