
Ashley Yakeley wrote:
I think it would be helpful if all these classes came with their laws
prominently attached in their Haddock documentation or wherever. The trouble with MonadPlus is that the precise set of associated laws is either unspecified or not the most useful (I assume there's a paper on the class somewhere). I think everyone can agree on these:
mplus mzero a = a mplus a mzero = a mplus (mplus a b) c = mplus a (mplus b c)
I think it would be even better if the classes came with assertions that 'enforced the laws'... I think this requires dependant types though.
mzero >>= a = mzero
But what about this?
a >> mzero = mzero
Well it was in the list I saw... I we consider the familar arithmetic product a * b * 0 -- it is clear that an mzero anywhere in a sequence should result in mzero: a >> b >> mzero >> c >> d = mzero But that says nothing about the co-product... where mzero should be the identity IE: a `mplus` mzero = a mzero `mplus` a = a But I am not sure there are any requirements on commutivity or associativity on the co-product operation?
It's satisfied by [] and Maybe, but not IO (for instance, when a is 'putStrLn "Hello"'), but IO has been declared an instance of MonadPlus. And then there are the two I gave:
(mplus a b) >>= c = mplus (a >>= c) (b >>= c)
This was not on the list I saw - guess it could either be an omission, or it has nothing to do with "MonadPlus" ... monads with identity and co-product?
...which is satisfied by [], but not Maybe or IO.
mplus (return a) b = return a
...which is satisfied by Maybe and IO, but not [], although your alternative declaration would make [] satisfy this and not the previous one.
But one could make up any arbitrary law that is satisfied by some definition of a Monad and not others. Presumably there has to be some sound category-theoretic reason for including the law? Keean