17 Oct
2010
17 Oct
'10
6:55 a.m.
On Sun, Oct 17, 2010 at 6:49 AM, 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
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.