My intention wasn't to add these laws, but to replace the existing MonadPlus ones. (Adding new laws wouldn't help with the original ones being invalid.) But you're right, the laws I proposed follow from Monad laws and from

mzero >>= f = mzero

This single law is enough to ensure that any chain of operations containing `mzero` "ends" at this point.

So the best solution seems to just remove the problematic

v >> mzero = mzero

2014-02-04 Dan Burton <danburton.email@gmail.com>:

I'm not sure what should be the proper solution. Perhaps to change the laws to:
return x >> mzero = mzero
(v >> mzero) >>= f = (v >> mzero)`
That is, if an expression ends with `mzero`, it behaves like `mzero`.

These laws are redundant with existing laws. The first:

return x >> z = z

Is true forall x and z, and can be proven by just the monad laws. The second:

(v >> mzero) >>= f = (v >> mzero)

Can be proven by the associativity of monadic operations:

(v >> mzero) >>= f = v >> (mzero >>= f)

And the other MonadPlus law already states that (mzero >>= f) = mzero. So I don't think any new laws are needed. I just think the (v >> mzero = mzero) law should be removed, or else a *lot* of instances of MonadPlus need to come with a disclaimer that they are not law-abiding.

-- Dan Burton