Am Sonntag, 23. Januar 2005 13:21 schrieb Keean Schupke:
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
Definitely!
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?
I'm afraid I don't understand what you mean by that. I know what a product and a coproduct are in any category, but that's obviously something completely different. In what way should one think of (>>) as a product? With lists, I can see a vague analogy, but in the IO-case, I can't, there I read a1 >> a2 as 'first do a1, then a2'. It's an associative law of composition, yes, but takes arguments of different types, and has no identity (lots of left identities, return whatever; but no right identity -- that's also true for lists and Maybe, by the way). So why make an analogy with ordinary multiplication?
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.
from an earlier message of Keean:
1. |mzero >>= f == mzero| 2. |m >>= (\x -> mzero) == mzero| 3. |mzero `mplus` m == m| 4. |m `mplus` mzero == m|
What exactly does 2. mean in the IO-case? a) the results of both calculations are equal -- then it also holds for IO. b) both produce the same output and the same result -- then it doesn't hold for IO. I think, a) is the correct interpretation.
And then there are the two I gave:
(mplus a b) >>= c = mplus (a >>= c) (b >>= c)
And what about x >>= (\y -> (c y) `mplus` (d y)) == (x >>= c) `mplus` (x >>= d) or, less general x >> (a `mplus` b) == (x >> a) `mplus` (x >> b)? This is satisfied for Maybe and IO, but not for [], where it's only true modulo a permutation. If we pair (>>) with (*) and `mplus` with (+), I find this a very natural law too. The problem is of course that neither (>>) nor `mplus` are commutative, so we shouldn't expect a strong analogy anyway.
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?
again, what do you mean by co-product? MonadPlus says simply that on every m a we have a monoid-structure. The laws 1. and 2. above relate one aspect of this structure with the Monad-structure, namely once we hit mzero, we can't get away from it (and it doesn't matter how we got there). Any stronger relation is sheer luck. We can do something pretty ugly with lists. instance MonadPlus [] where mzero = [] [] `mplus` lis = lis lis `mplus` [] = lis l1 `mplus` l2 = take 3 (l1 ++ l2) Now mplus (return 1) [2,3] == [1,2,3]; (mplus [1,2] [3,4]) >> [5,6] == [5,6,5,6,5,6]; ([1,2] >> [5,6]) `mplus` ([3,4] >> [5,6]) == [5,6,5]; [1,2] >> ([3] `mplus` [4]) == [3,4,3,4]; ([1,2] >> [3]) `mplus` ([1,2]>>[4]) == [3,3,4]. So none of the -more or less natural- relations discussed so far holds in this case.
...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
Well, one might prescribe any set of rules that should be satisfied by a MonadPlus, then any instance declaration violating one of them would be -what? Bad style at least. But it's the same with Functor or Monad, no way to guarantee the laws. I suppose, if in category theory there was a definition of MonadPlus requiring additional laws, they would have been included in the above list and no offending instances would have been declared. By the way, does anybody know any sources where a non-category-theorist can learn what Monad and MonadPlus are? (Functors, of course, but what sort?) Daniel