[Haskell-cafe] Proving stuff about IORefs
Derek Elkins
derek.a.elkins at gmail.com
Sun Oct 17 06:55:42 EDT 2010
On Sun, Oct 17, 2010 at 6:49 AM, Miguel Mitrofanov
<miguelimo38 at yandex.ru> 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.
More information about the Haskell-Cafe
mailing list