[Haskell-cafe] Proving stuff about IORefs

[Miguel Mitrofanov]

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.