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.