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

[Daniel Fischer]

Am Montag, 24. Januar 2005 11:47 schrieb Jules Bean:
<snip>
> Here are the three monad laws as written on the nomaware site:
>
> 	1.  	(return x) >>= f == f x
> 	2.  	m >>= return == m
> 	3.  	(m >>= f) >>= g == m >>= (\x -> f x >>= g)
>
> Taking rule 1, we do not simply mean that return x >>= f and f x have
> the same type. (This is obviously true). We require that they are equal
> as values of the type m a. In the case of IO, this means that they
> perform the same action before yielding the same result.

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.
The sad truth is that IO actions in general aren't well defined entities 
(unless we index them with the space-time-coordinates of their invocation).
So I suggest ending the discussion by agreeing that the question whether or 
not
x >> mzero == mzero
holds in the IO-Monad is meaningless (at least, it's fruitless).
If you cannot agree, I have another question: is

return 4 >> return 5 == return 5

true in the IO-Monad?
From the 'just the result matters'-point of view, obviously.
From the 'everything matters'-point of view not.

I feel a little more at home with the former, because it matches the 
extensional equality of set theory, but I'm not happy with either.
For any mathematician, the function
\x -> 2*sin x * cos x
IS the same function as
\x -> sin (2*x)
(given the equality of their respective domains -- though, for ghc they 
aren't, due to rounding errors), so if we transport this extensionality to 
our problem -- I am aware that is problematical because of the side-effects 
-- we get 
putStrLn "hello" >> mzero == mzero.

>
> Example:
>
> return "hello" >>= putStrLn
>
> this does not only have the same type as putStrLn "hello", and return
> the same value (), but it also carries out exactly the same actions.

But does it really? hugs thinks otherwise:
Prelude> putStrLn "hello"
hello
()
(28 reductions, 55 cells)
Prelude> return "hello" >>= putStrLn
hello
()
(31 reductions, 56 cells)
Prelude> putStrLn "hello"
hello
()
(26 reductions, 50 cells)

even the same input does not necessarily lead to exactly the same actions, 
depending on whether "hello" is already known or not.
>
> If it was simply enough that it have the same type, then it would be
> 'good enough' if
>
> return "hello" >>= putStrLn
>
> had the same effect as
>
> putStrLn "goodbye"
>
> ...which has the same type, and the same return value.

Yes, definitely a point, if only the result matters, we must say
putStrLn "hello" == putStrLn "goodbye",
which is somewhat counterintuitive. On the other hand, there are many 
counterintuitive truths around.
>
> Aside: you said a couple of messages ago:
> > Yes it is, side effects are quite clearly not counted. The value
> > of (putStrLn "Hello" >> mzero") is mzero.
>
> This concept of 'value' only makes sense in some monads. In the List
> monad there can be many 'values' of a computation. It just happens that
> IO 'returns' a 'single value' all the time.

Yes, and return "hello" returns the value "hello", so the concept of value 
absolutely makes sense in the IO-Monad -- though I would prefer to call 
"hello" the 'result' of the IO-action, rather than the 'value'. And the 
result of x >> mzero is mzero, regardless of what x is.

Keean:
>Just thinking about this, a monad is a Functor plus two 
>natural-tranformations, Unit and Join. Is there an equivalent definition 
>for MonadPlus... I am not sure I understand where MonadPlus comes from? 
>Is it just a Functor and two different definitions of Unit and Join 
>(from those chosen to be in the class Monad?)
>
>    Keean.
And these two transformations must satisfy certain conditions.
As for MonadPlus, it's just a Monad m with the additional property that 
forall objects a, the object m(a) is a monoid -- if I'm not mistaken, it also 
defines a Functor into the category of monoids in our three cases and should 
do anyway (that's something different from the fact that the object m(a) is a 
monoid, additionally we must have that for all maps f: a -> b, the associated 
map fmap f (which should be liftM f) is a monoid-homomorphism; however if we 
view m as a functor into category Mon, it is no longer a Monad, because then 
even the concept of a natural transformation of Id to m isn't defined, since 
these are functors to different categories).
I haven't yet figured out, why exactly mzero >> x and x >> mzero must always 
yield mzero, that is, the exact interplay between 'bind' and 'fmap', but in 
our three cases it's natural enough (pace Ashley, Jules and everybody else: 
if we take the 'results only'-point of view).

Aside:
>In reference to the idea of splitting MonadPlus, what category
>would you be operating in, if you have a zero but 
>no co-product operation?                                                            
  ^^^^^^^^^^^^^^^^^^^^^^
I ask again: what is a co-product operation?
Can't be the operation of forming the coproduct of a family of objects in a 
category, sounds like some sort of operation on an object (that would usually 
be a map ob -> ob -> ob), but I don't know the term, so could someone please 
explain?

Ashley:
>If you remember your category theory, you'll recall that two morphisms 
>are not necessarily the same just because they're between the same two 
>objects. For instance, the objects may be sets, and the morphisms may be 
>functions between sets: morphisms from A to B are the same only if they 
>map each element in A to the same element in B.

Yes, and if your set theory is (for example) NBG without atoms, every object 
(being an element of a class) is a set, in particular this holds for IO a, so 
then the question of whether or not
putStrLn "hello" >> mzero == mzero
hasn't anything to do with functors or category theory, it's just part of the 
question 'when do you call two elements of IO a equal?' Categories and Monads 
enter the picture only when we progress to the next question:
'is x >> mzero == mzero necessarily true for all x?'
The answer to the second question of course depends on the answer to the 
first. If category theory says the answer to the second is yes for any 
Monad(Plus), but we have
putStrLn "hello" >> mzero /= mzero, well, then IO isn't a Monad(Plus). However 
it'd still be useful to pretend it were, I suppose.

But I'm still unsure about the first question.
And I spend too much time thinking about it.

Daniel