[Haskell-cafe] A law for MonadReader

[Li-yao Xia]

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