[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"
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
More information about the Haskell-Cafe
mailing list