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. |

- Re: Laws for Monads with zero and plus Koen Claessen
- Re: Laws for Monads with zero and plus Philip Wadler
- Re: Laws for Monads with zero and plus Koen Claessen
- Re: Laws for Monads with zero and plus John C. Peterson
- Re: Laws for Monads with zero and plus Tony Davie
- Re: Laws for Monads with zero and plus reid-alastair
- Re: Laws for Monads with zero and plus Hans Aberg