[Haskell-cafe] Proving stuff about IORefs
matthew at brecknell.net
Sun Oct 17 08:29:32 EDT 2010
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
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
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.
More information about the Haskell-Cafe