On 06/03/2018 03:32 AM, Benjamin Fox wrote:
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.
Thanks Benjamin, that's a good counterexample. It also shows that the other missing implications (((3) => (4)) and ((3) => (2))) do not hold. Indeed, I had incorrectly assumed that even if we discard the result of an action, we can reconstruct it by observing the action's effects, and (1) and (3) were meant to imply that those effects must be trivial, but newIORef contradicts this because the creation of a new reference is only made observable by using it. Li-yao