[Haskell-cafe] A law for MonadReader
lysxia at gmail.com
Sun Jun 3 00:18:41 UTC 2018
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
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