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

On Wed, Feb 5, 2014 at 8:38 PM, John Lato wrote:

On Wed, Feb 5, 2014 at 5:01 PM, wren ng thornton wrote:

...

On Wed, Feb 5, 2014 at 7:59 PM, wren ng thornton wrote:

...

The rules I'd expect MonadPlus to obey are:

mzero >>= f = mzero

(x `mplus` y) >> mzero = (x >> mzero) `mplus` (y >> mzero)

Er, sorry, that should've been:

(x `mplus` y) >> z = (x >> z) `mplus` (y >> z)

from which the above instance follows trivially.

I don't think this is correct. [...] Or concretely,

...

let x = lift (print "x!") :: MaybeT IO () let y = lift (print "y!") :: MaybeT IO () runMaybeT $ (x `mplus` y) >> mzero

"x!" Nothing

...

runMaybeT $ (x >> mzero) `mplus` (y >> mzero)

"x!" "y!" Nothing

Well, notably, the Maybe part of things does agree. It's the transformer part which breaks things. However, this is something that could be "fixed" by changing the implementation of mplus for MaybeT. In particular, if we have it fully execute both arguments, but then discard the results of latter ones whenever earlier ones have succeeded. That is, mplus x y = MaybeT $ do v <- runMaybeT x w <- runMaybeT y case v of Nothing -> return w Just _ -> return v This "fix" ensures that the law is obeyed regardless of the underlying monad. However, it's not necessarily the instance we want. So the question is: for monad transformers, what --explicitly, concretely-- do we want? Do we consider the current MaybeT instance sacrosanct? What about the other popular instances? I still think the above laws are the most sensible ones. I discuss a bit about why I believe that in this blog post I just posted[1]. The only alternative I see is to drop every law about how mplus interacts with bind, which isn't a solution quite so much as giving up. [1] http://winterkoninkje.dreamwidth.org/90905.html -- Live well, ~wren