Petr Pudlák petr.mvd at gmail.com
Tue Feb 4 08:21:25 UTC 2014

```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 at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...