As far as I can tell, (1) on it's own does not imply (2). I even have a counterexample, assuming no further laws on `ask` and no laws on `local`. Requiring `local` makes things more complicated (as `local` always does) and it may well be that a sufficiently strong law for `local` would rule out cases where (1) and (2) differ. (I'm not sure of that, I'll need to think about it a bit more.) Here is the counterexample: instance MonadReader (IORef Int) IO where ask = newIORef 0 local _ = id This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0. But not (2): (newIORef 0 >>= \r1 -> newIORef 0 >>= \r2 -> return (r1, r2)) ≠ (newIORef 0
= \r -> return (r, r)). The left side of (2) returns a tuple containing two different IORefs (both containing 0), whereas the right side returns a tuple containing two references to the same IORef.
On Sun, Jun 3, 2018 at 2:19 AM Li-yao Xia
Hello Café,
While trying to document laws for mtl classes (https://github.com/haskell/mtl/issues/5) I have been puzzling over the subtle logical relationships between a few variants.
Consider the following four possible laws for MonadReader's ask:
(1) (ask >> ask) = ask
(2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r -> return (r, r))
(3) (ask >> return ()) = return ()
Let
reader :: MonadReader r m => (r -> a) -> m a reader f = fmap f ask
(4) reader is a monad homomorphism from ((->) r) to m, i.e.:
reader (\_ -> a) = return a (reader m >>= \x -> reader (k x)) = reader (m >>= k)
Question: which ones imply which ones?
Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2) say that ask is idempotent ("asking twice is the same as asking once"), but (3) and (4) imply the stronger property of nullipotence ("ask has no side effects").
---
Any help with the following conjectures is welcome (we're assuming the monad laws hold in the first place):
A. (1) and (2) are equivalent.
I can prove that (2) implies (1). However the converse eludes me.
B. (3) and (4) are equivalent.
Again, I can prove that (4) implies (3), but I had no success with the converse.
C. ((3) or (4)) implies ((1) and (2))
((3) implies (1)), and ((4) implies ((1) and (2))) are straightforward, but without the above equivalence, the missing bit is ((3) implies (2))
It seems that parametricity plays an important role in the conjectured implications. I didn't manage to apply free theorems to this problem, but perhaps you will have better luck.
Regards, Li-yao _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.