[Haskell-cafe] A law for MonadReader

[Benjamin Fox]

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 ()
>
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180603/08593569/attachment.html>