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

[Dan Burton]

Indeed this issue is not limited merely to multiple failure values.

    >>> runMaybeT $ lift (putStrLn "effect") >> mzero
    effect
    >>> runMaybeT mzero


So you're right. This law is being violated

-- Dan Burton


On Mon, Feb 3, 2014 at 12:21 PM, Petr Pudlák <petr.mvd at gmail.com> wrote:

> Since nobody replied so far, I'm also forwarding to cafe.
> Petr
>
>
> ---------- Forwarded message ----------
> From: Petr Pudlák <petr.mvd at gmail.com>
> Date: 2014-01-29
> Subject: incorrect MonadPlus law "v >> mzero = mzero"?
> To: "libraries at haskell.org" <libraries at haskell.org>
>
>
> Hi,
>
> this law apparently fails for a MonadPlus instance that has more than one
> possible failure value. Consider:
>
>    runIdentity . runErrorT $
>     ((ErrorT . Identity $ Left "failure") >> mzero :: ErrorT String
> Identity ())
>
> evaluates to `Left "failure"`, which isn't equal to ErrorT's mzero `Left
> ""`.
>
> This isn't just the case of ErrorT, it fails for any MonadPlus with
> multiple failure values. For example
>
>   lift (tell "foo") >> mzero :: MaybeT (Writer String) ()
>
> is again distinct from mzero.
>
> Actually, no monad transformer with a MonadPlus instance can satisfy the
> law, because the first part in front of `>> mzero` can introduce side
> effects in the underlying monad.
>
> 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`.
>
>   Petr
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140203/8f43a742/attachment.html>