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.
In Haskell, a Monad is represented by the following class:
class Monad m where
(>>=) :: 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:
class Monad m => MonadZero m where
zero :: m a
And for plus:
class MonadZero m => MonadPlus m where
(++) :: 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. |
