I have a formal proof where I am stuck at a certain point.
Suppose we have a function
f :: IORef a -> IO b
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
What happens here is that the temporary IORef r' takes the place of the
argument r, and after we apply f to it we take its content and store it in
the original r. This should be the same as using r as argument to f in the
first place.
How can I prove this formally?
Cheers
Ben
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
