[Haskell-cafe] Proving stuff about IORefs

[Matthew Brecknell]

Hi Ben,

Ben Franksen wrote:
> 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

I'm not sure where in your question the quantifiers for types a and b
are intended to be.

If you really do mean:

"Given an arbitrary function f with polymorphic type
f :: forall a b. IORef a -> IO b
prove that..."

then you might be able to appeal to parametricity. I wouldn't know how
to apply parametricity to IO actions, though.

On the other hand, Miguel and Derek seem to be interpreting these as
meta-variables which are quantified over the whole question; in other
words, that you mean:

"Given arbitrary types A and B, and a function
f :: IORef A -> IO B
prove that..."

Derek's counter-example is then, more explicitly:

type A = ()
type B = IORef ()
f = return

If I had time to digest your second post, I might be able to figure out
which of these (plus a couple of other possibilities) is required. So my
point is just that if you don't think about these things explicitly,
it's easy to unwittingly make an assumption, possibly to the detriment
of whatever you're trying to achieve.

Regards,
Matthew