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