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

[Daniel Fischer]

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