[Haskell-cafe] Fwd: incorrect MonadPlus law "v >> mzero = mzero"?

[Petr Pudlák]

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...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140204/f899b281/attachment-0001.html>