[Haskell-cafe] Re: What are the MonadPlus laws?

[Jules Bean]

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 
arrows (computations).

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.

Jules