Fwd: incorrect MonadPlus law "v >> mzero = mzero"?
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
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@gmail.com> wrote:
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
On Mon, Feb 3, 2014 at 5:51 PM, Dan Burton <danburton.email@gmail.com>wrote:
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
I thought it was fairly well known that IO violates one of the monad laws, in a way that would lead to this? -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
On Mon, Feb 3, 2014 at 3:00 PM, Brandon Allbery <allbery.b@gmail.com> wrote:
On Mon, Feb 3, 2014 at 5:51 PM, Dan Burton <danburton.email@gmail.com>wrote:
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
I thought it was fairly well known that IO violates one of the monad laws, in a way that would lead to this?
The choice of IO for the underlying monad is irrelevant. The issue is that a later mzero in the transformer cannot undo an earlier action in a lower monad. For example:
Prelude Control.Monad.Maybe Control.Monad.State> runStateT (runMaybeT $ (lift $ put "bar") >> mzero) "foo" (Nothing,"bar") Prelude Control.Monad.Maybe Control.Monad.State> runStateT (runMaybeT mzero) "foo" (Nothing,"foo")
The issue is that a later mzero in the transformer cannot undo an earlier action in a lower monad.
Precisely. Another example, for fun:
print (runMaybeT $ lift [1,2,3] >> mzero :: [Maybe Int]) [Nothing, Nothing, Nothing]
print (runMaybeT mzero :: [Maybe Int]) [Nothing]
Actually, I'd say the problem *isn't *that a transformer "cannot undo earlier action in a lower monad." I'd just say that most transformers *happen to be implemented *in this "forgetful" manner. It's conceivable that we could implement some of them differently, in a way that would obey the MonadPlus laws. Whether or not obedience to this particular law is worthwhile... well, that's debatable. -- Dan Burton
I would argue that a monad transformer "cannot undo earlier action in a lower monad." For example, in the case of MaybeT: In order to determine of an action succeeded or failed, it needs to evaluate in the underlying monad. But what if the underlying monad doesn't provide any means to restore its state to some previous point? So I believe having 'v >> mzero = mzero' for a transformer with MonadPlus would be only possible if the underlying monad provided some kind of check-pointing. 2014-02-04 Dan Burton <danburton.email@gmail.com>:
The issue is that a later mzero in the transformer cannot undo an earlier
action in a lower monad.
Precisely. Another example, for fun:
print (runMaybeT $ lift [1,2,3] >> mzero :: [Maybe Int]) [Nothing, Nothing, Nothing]
print (runMaybeT mzero :: [Maybe Int]) [Nothing]
Actually, I'd say the problem *isn't *that a transformer "cannot undo earlier action in a lower monad." I'd just say that most transformers *happen to be implemented *in this "forgetful" manner. It's conceivable that we could implement some of them differently, in a way that would obey the MonadPlus laws. Whether or not obedience to this particular law is worthwhile... well, that's debatable.
-- Dan Burton
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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@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
participants (4)
-
Brandon Allbery -
Dan Burton -
John Lato -
Petr Pudlák