[Haskell-cafe] Re: What are the MonadPlus laws?
jules at jellybean.co.uk
Wed Jan 26 07:50:49 EST 2005
On 26 Jan 2005, at 08:41, Keean Schupke wrote:
> I cannot find any reference to MonadPlus in category theory. At a
> guess I would say that
> it was the same as a Monad except the operators are id and co-product
> (or sum)... That would mean the 'laws' would be exactly the same as a
> Monad, just with (0,+) instead of (1,*)...
I don't know if the categorists have a word for it. It isn't "the same
as a Monad except", it's rather "the same as a Monad and also...". Note
that translating between the normal categorical point of view and the
haskell one is something of a pain since programmers think with Kleisli
A MonadPlus is a Monad T with, in addition, the structure of a monoid
on all types T a, satisfying the some conditions. I follow Wadler and
use zero and ++ for the monoid.
Unit conditions: If you apply a monadic computation (that is, Kleisli
arrow) to the zero object you get zero, that there is a special zero
computation (that is concretely \x -> zero) which gives you the zero
object when you apply it to anything.
Compatibility of ++ with computations:
The first condition just says that if you apply a computation to the
sum of two objects, that should be the same as applying the computation
twice, once to each object, and adding the results.
(m ++ n) >>= f == (m >>= f) ++ (n >>= f)
The two slightly more subtle conditions observe that it is possible to
'lift' the monoid operation to Kleisli arrows, i.e. if you can add
objects, then you can add computations (of the same type):
(+++) : (a -> m b) -> (a -> m b) -> (a -> m b)
\f g x -> f x ++ g x
Then you require that if you first add two computations and apply them
to a single object, you get the same result as applying the
computations separately and adding the results..
m >>= (f +++ g) == (m >>= f) ++ (m >>= g)
If these are a common categorical notion then I'd expect them to be
called 'additive monads' or something, but I can't immediately track
down a reference.
If you translate the notion back to the more standard categorical
approach, using mu (join) and eta (return), it may be enlightening, but
off hand I can't quite see what the rules look like.
More information about the Haskell-Cafe