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