On Wed, Jan 29, 2014 at 8:57 AM, Petr Pudlák
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`.
As others've mentioned, these come for free from being a monad together with (mzero >>= f) = mzero. The rules I'd expect MonadPlus to obey are: mzero >>= f = mzero (x `mplus` y) >> mzero = (x >> mzero) `mplus` (y >> mzero) x `mplus` (y `mplus` z) = (x `mplus` y) `mplus` z x `mplus` mzero = x mzero `mplus` y = y The last three simply state that (mplus,mzero) forms a monoid. The first two laws indicate that the (>>) notion of "multiplication" distributes over the mplus notion of "addition", but only from the right side. These laws together with the associativity of (>>) mean that MonadPlus forms a right-seminearring (or right-nearsemiring, if you prefer). If we additionally require that mplus is commutative, then its an commutative right-seminearring. Seminearrings show up naturally all over the place, especially in linguistic contexts (i.e., parsing and generation of "strings"). I know Edward Kmett has talked about them before, and other algebraically minded folks are probably familiar with them too. They're one of my favorites and not too much more difficult to work with than semirings. ObTangent: For the algebraically minded, we have that S is a semiring just in case (1) S is a right-seminearring (2) S is a left-seminearring (just flip the directionality of the first two laws above) (3) the addition of S is commutative (4) there exists an identity element for multiplication -- Live well, ~wren