[Haskell-cafe] Re: what is inverse of mzero and return?
daniel.is.fischer at web.de
Sun Jan 23 13:34:01 EST 2005
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
> >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
> > mzero >>= a = mzero
> >But what about this?
> > a >> mzero = mzero
> Well it was in the list I saw... I we consider the familar arithmetic
> 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
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
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
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)
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] >> ( `mplus` ) == [3,4,3,4];
([1,2] >> ) `mplus` ([1,2]>>) == [3,3,4].
So none of the -more or less natural- relations discussed so far holds in this
> >...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
> 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?
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?)
More information about the Haskell-Cafe