Am Montag, 24. Januar 2005 20:25 schrieb Keean Schupke:
I think the endofunctors are defined on the types, not the values though. So the object of the category is the endofunctor (Type -> Type), and unit and join are the identity and binary associative operator on which a Monad is defined. return and bind are defined in terms of unit and join. So unit is the identity which when joined to the endofunctor (Type -> Type) results in the same endofunctor... Therefor:
(Type -> Type) `join` unit => (Type -> Type)
Now as the type of the IO monad is "IO a" we end up with:
(IO a -> IO a) `join` unit => (IO a -> IO a)
This is true irrespective of any side effects IO may have, as the type is the same for the IO action no matter what side effects it generates.
At least thats how I understand it...
Keean.
You lost me there. As I see it, the objects of C are the types, i.e. Ob(C) = {T : T is a Haskell type}. I'd say that a type is a set of values, but that doesn't matter really. The Morphisms of C are the functions between types, i.e. Mor(A, B) = {f : A -> B}. Then IO is (supposed to be) a functor C -> C, that is, to every object A we have an associated one, namely IO(A), and to every morphism f `elem` Mor(A,B) we have an associated one, IO(f) `elem` Mor(IO(A), IO(B)). Further we have a natural transformation, eta, from the identity functor to IO, that is, for every A `elem` Ob(C) we have an eta_A `elem` Mor(A, IO(A)), such that (forall A,B `elem` Ob(C)) (forall f `elem` Mor(A, B)) (eta_B . f == IO(f) . eta_A) and a natural transformation mu from IO . IO to IO, that is, for every A `elem` Ob(C) we have a mu_A `elem` Mor(IO(IO(A)), IO(A)), such that (forall A,B `elem` Ob(C)) (forall f `elem` Mor(A, B)) (mu_B . IO(IO(f)) == IO(f) . mu_A). Now, eta is return and mu is join, or mu_A = (>>= id_(IO(A))). Finally, in order to make the triple (IO, eta, mu) a Monad, eta and mu must meet three conditions: i) mu . IO(mu) = mu . mu, or, more clearly (forall A `elem` Ob(C)) (mu_A . IO(mu_A) == mu_A . mu_(IO(A))), ii) mu . eta == id, or (forall A `elem` Ob(C)) (mu_A . eta_(IO(A)) == id_(IO(A))), iii) mu . IO(eta) == id, or (forall A `elem` Ob(C)) (mu_A . IO(eta_A) == id_(IO(A))). Each of these conditions demands the equality of some functions, and all of these functions are in Mor(A, IO(B)) for appropriate A and B. So the first question to answer -- and I believe the rest will relatively easily follow from that answer -- is What does equality mean in type IO(A)? Without that, the conditions are meaningless, and IO cannot even be a functor. And suppose we found an answer, such that indeed IO is a functor. Are then conditions i)--iii) fulfilled? Condition ii) demands that return (putStrLn "hi") >>= id == putStrLn "hi". Let's try it out: Prelude> putStrLn "hi" hi (16 reductions, 30 cells) Prelude> return (putStrLn "hi") >>= id hi (22 reductions, 36 cells) Now obviously they aren't absolutely identical, in return .. >>= id, we execute the actions of first wrapping up putStrLn "hi" in a further IO-layer and then unwrapping it again. So if we insist that equality of IO-actions means that exactly the same actions are performed, IO is NOT a Monad. But I don't suppose such a rigid interpretation was intended and in our running example, there was additional output generated, which is a visible difference. But is it so important whether WE see a difference or only the machine does? Of course, saying that two IO-actions are equal when they return the same result (given the same input), is not easily accepted, but output isn't the perfect criterion either: what if stdout is closed? Is putStrLn "hello" >> mzero == mzero then? I wish someone called Simon could shed some light on this issue. Daniel