Since nobody replied so far, I'm also forwarding to cafe.
Petr

---------- Forwarded message ----------
From: Petr Pudlák <petr.mvd@gmail.com>
Date: 2014-01-29
Subject: incorrect MonadPlus law "v >> mzero = mzero"?
To: "libraries@haskell.org" <libraries@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe