incorrect MonadPlus law "v >> mzero = mzero"?

[wren ng thornton]

On Wed, Jan 29, 2014 at 8:57 AM, Petr Pudlák <petr.mvd at gmail.com> wrote:
> 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