Li-yao Xia lysxia at gmail.com
Sun Jun 3 00:18:41 UTC 2018

```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.

(2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r ->
return (r, r))

(3) (ask >> return ()) = return ()

Let

(4) reader is a monad homomorphism from ((->) r) to m, i.e.:

reader (\_ -> a) = return a

Question: which ones imply which ones?

Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2)
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
```