On Sun, Oct 17, 2010 at 6:49 AM, Miguel Mitrofanov <[email protected]> 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. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
