# Laws for Monads with zero and plus

```
It is my hobby to play around with Monads and look at their properties
:-). Recently I defined a Monad with a zero and a plus and wanted to prove
that the laws for zero and plus held for my Monad. To my surprise, I
couldn't find any document that described these laws in detail.

(>>=)  :: m a -> (a -> m b) -> m b
return :: a -> m a

For these operators, the Three Monad Laws should hold:

1. return x >>= f           ===  f x
2. m >>= return             ===  m
[Left and Right unit]

3. m >>= (\x -> f x >>= g)  ===  (m >>= (\x -> f x)) >>= g
[Associativity of >>=]

So far nothing new or surprising.

Further, a Monad can have a so-called zero or even a plus. In Haskell,
this is expressed by the following class for zero:

zero :: m a

And for plus:

(++) :: m a -> m a -> m a

Note that a Monad should have a zero before it can have a plus. The
following laws express the relationship between zero and plus:

4. m    ++ zero    ===  m
5. zero ++ m       ===  m
[Left and Right unit]

Further, there is at least one law that expresses the relationship between
>>= and ++:

6. (m ++ n) >>= f  ===  (m >>= f) ++ (n >>= f)
[Right distibution of >>= over ++]

At this point my knowledge (and the knowledge of the people and papers
accessible for me) stops. Several questions remain:

i) It is possible to have a Monad with a zero, but without a plus. There
are no laws known to me that involve zero but not plus. Two laws seem
applicable:

7?. zero >>= f         ===  zero
[Left zero]

8?. m >>= \_ -> zero   ===  zero
[Right zero]

All Monads with a zero I know of obey the first law (7?). But I can
think of Monads with a perfectly suitable zero for which (8?) doesn't
hold, for example:

type W a = (Maybe a, String)

bindW :: W a -> (a -> W b) -> W b
(Just a, s)  `bindW` k = let (mb, s') = k a in (mb, s++s')
(Nothing, s) `bindW` k = (Nothing, s)

zeroW :: W a
zeroW = (Nothing, "")

There are two possible conclusions:

a) Law (8?) holds, and zeroW, which seems perfectly alright, is not
a zero for W after all;
b) Law (8?) doesn't hold, so there seems to be an a-symmetry in the
laws that is not expressed in other laws.

That brings us to the second question.

ii) If there is an a-symmetry in the laws for zero, is there also one in
the laws for plus? In other words, does the following law hold:

9?. m >>= \x -> (n ++ k)  ===  (m >>= \x -> n) ++ (m >>= \x -> k)
[Left distribution of >>= over ++]

There are two possible cases:

a) The law doesn't hold, in which case everything makes perfect
sense if (7?) hold in general as well;
b) The law does hold, in which case there is an a-symmetry that
doesn't make sense (note that this is not a proof, but a
motivation):

- We generalize (6) to:

(SIGMA m_i) >>= f  ===  SIGMA (m_i >>= f)

And conclude, for the nullary SIGMA, that:

zero        >>= f  ===  zero

- But then we can also generalize (9?) to:

m >>= \x -> SIGMA n_i  ===  SIGMA (m >>= \x -> n_i)

And conclude, for nullary SIGMA:

m >>= \x -> zero       ===  zero

So, there seems to be a connection between law (9?) and law (7?).

Who can enlighten me in this matter?

Thanks,
Koen.

--
|  Koen Claessen,                   [EMAIL PROTECTED]  |
|                   http://www.cse.ogi.edu/~kcclaess/  |
|------------------------------------------------------|
|  Visiting student at OGI,    Portland, Oregon, USA.  |

```