[Haskell-cafe] A law for MonadReader

[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