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 <lysxia@gmail.com> wrote:
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.