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

       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

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


|  Koen Claessen,                   [EMAIL PROTECTED]  |
|           |
|  Visiting student at OGI,    Portland, Oregon, USA.  |

Reply via email to