[Haskell-cafe] Proving stuff about IORefs

Thomas DuBuisson thomas.dubuisson at gmail.com
Sat Oct 16 22:22:59 EDT 2010

I must be missing the point of the proof.  The value of 'f r' is _|_.
Practically speaking, it will eventually stack overflow.  Why is
proving anything about this interesting?  Why do you think the store
will ever happen on the original r?


On Sat, Oct 16, 2010 at 6:21 PM, Ben Franksen <ben.franksen at online.de> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list