[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 ()
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
More information about the Haskell-Cafe
mailing list