[Haskell-cafe] A law for MonadReader
foxbenjaminfox at gmail.com
Sun Jun 3 07:32:29 UTC 2018
As far as I can tell, (1) on it's own does not imply (2). I even have a
counterexample, assuming no further laws on `ask` and no laws on `local`.
Requiring `local` makes things more complicated (as `local` always does)
and it may well be that a sufficiently strong law for `local` would rule
out cases where (1) and (2) differ. (I'm not sure of that, I'll need to
think about it a bit more.)
Here is the counterexample:
instance MonadReader (IORef Int) IO where
ask = newIORef 0
local _ = id
This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0. But not (2):
(newIORef 0 >>= \r1 -> newIORef 0 >>= \r2 -> return (r1, r2)) ≠ (newIORef 0
>>= \r -> return (r, r)). The left side of (2) returns a tuple containing
two different IORefs (both containing 0), whereas the right side returns a
tuple containing two references to the same IORef.
On Sun, Jun 3, 2018 at 2:19 AM Li-yao Xia <lysxia at gmail.com> wrote:
> 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.
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe