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

Daniel Fischer daniel.is.fischer at web.de
Mon Jan 24 17:38:23 EST 2005

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"

(16 reductions, 30 cells)
Prelude> return (putStrLn "hi") >>= id

(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.


More information about the Haskell-Cafe mailing list