<div dir="ltr"><div>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.)<br><br></div><div>Here is the counterexample:<br><br></div><div>instance MonadReader (IORef Int) IO where<br></div><div>    ask = newIORef 0<br></div><div>    local _ = id<br><br></div><div>This obeys law (1): (newIORef 0 >> newIORef 0) == newIORef 0. But not (2): (newIORef 0 >>= \r1 -> newIORef 0 >>= \r2 -> return (r1, r2))<font size="2"><span style="font-weight:normal"><span id="inbox-inbox-qTUjyD"><span class="inbox-inbox-ui_story_title inbox-inbox-ui_story_title_large"><span class="inbox-inbox-ui_qtext_rendered_qtext"> ≠</span></span></span></span></font> (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.<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Sun, Jun 3, 2018 at 2:19 AM Li-yao Xia <<a href="mailto:lysxia@gmail.com">lysxia@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Café,<br>
<br>
While trying to document laws for mtl classes <br>
(<a href="https://github.com/haskell/mtl/issues/5" rel="noreferrer" target="_blank">https://github.com/haskell/mtl/issues/5</a>) I have been puzzling over the <br>
subtle logical relationships between a few variants.<br>
<br>
Consider the following four possible laws for MonadReader's ask:<br>
<br>
(1) (ask >> ask) = ask<br>
<br>
(2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r -> <br>
return (r, r))<br>
<br>
(3) (ask >> return ()) = return ()<br>
<br>
Let<br>
<br>
reader :: MonadReader r m => (r -> a) -> m a<br>
reader f = fmap f ask<br>
<br>
(4) reader is a monad homomorphism from ((->) r) to m, i.e.:<br>
<br>
reader (\_ -> a) = return a<br>
(reader m >>= \x -> reader (k x)) = reader (m >>= k)<br>
<br>
Question: which ones imply which ones?<br>
<br>
Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2) <br>
say that ask is idempotent ("asking twice is the same as asking once"), <br>
but (3) and (4) imply the stronger property of nullipotence ("ask has no <br>
side effects").<br>
<br>
---<br>
<br>
Any help with the following conjectures is welcome (we're assuming the <br>
monad laws hold in the first place):<br>
<br>
A. (1) and (2) are equivalent.<br>
<br>
I can prove that (2) implies (1). However the converse eludes me.<br>
<br>
B. (3) and (4) are equivalent.<br>
<br>
Again, I can prove that (4) implies (3), but I had no success with the <br>
converse.<br>
<br>
C. ((3) or (4)) implies ((1) and (2))<br>
<br>
((3) implies (1)), and ((4) implies ((1) and (2))) are straightforward, <br>
but without the above equivalence, the missing bit is ((3) implies (2))<br>
<br>
It seems that parametricity plays an important role in the conjectured <br>
implications. I didn't manage to apply free theorems to this problem, <br>
but perhaps you will have better luck.<br>
<br>
Regards,<br>
Li-yao<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>