Benjamin Fox 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:

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.
>
>
>
> (2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r ->
> return (r, r))
>
> (3) (ask >> return ()) = return ()
>
> Let
>
>
> (4) reader is a monad homomorphism from ((->) r) to m, i.e.:
>
> reader (\_ -> a) = return a
>
> Question: which ones imply which ones?
>
> Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2)
> 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
> _______________________________________________