[Haskell-cafe] Re: Proving stuff about IORefs

Derek Elkins wrote:

On Sun, Oct 17, 2010 at 6:49 AM, Miguel Mitrofanov wrote:

...

On 17 Oct 2010, at 05:21, Ben Franksen wrote:

...

I want to prove that

f r == do s1 <- readIORef r r' <- newIORef s1 x <- f r' s3 <- readIORef r' writeIORef r s3 return x

That is not true. Consider the following function:

g r1 r2 = writeIORef r1 0 >> writeIORef r2 1 >> readIORef r1

This function behaves differently depending on whether r1 and r2 are the same IORef or not. Therefore, the property you want to prove doesn't hold for the partially-applied function

f = g r1

I originally was thinking along these lines, and this is an important case, but there is an even more trivial example.

Let f be return.

Oh, my god. Of course. Thanks for pointing me to the obvious ;-) This means I either have to give up on the second law callback . embed = id or find another implementation. Maybe IORef is too powerful. Hmm. The second law was inspired by the instance for ReaderT: instance Embed m (ReaderT r m) where type Content m (ReaderT r m) = r embed = ReaderT callback = runReaderT which is much more general (it does not depend on the inner monad being IO), and where indeed the second law holds. Cheers Ben