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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe