[Haskell-cafe] A law for MonadReader

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.

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 ()


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 

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.


More information about the Haskell-Cafe mailing list