Hi Mathew Matthew Brecknell wrote:
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.
No, I would have written this explicitly as f :: forall a b. IORef a -> IO b . I thought it is the generally accepted convention that free variables appearing in a proposition are understood to be universally quantified (at the outermost level). If we had to always explicitly write down all the quantifiers, formulas would quickly become unwieldy.
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.
Right, in general. That wasn't my mistake, though. I just wanted the law to hold so badly I forgot that IORefs have an identity separate from what their content is, so even if what the do-block returns has the same content, it is still a different IORef. However, I have the notion now that it suffices to prove something much weaker, namely callback . embed . const = id Note that this is a special case of the original law callback . embed = id It means that the IO action does not get passed a reference and thus I need only prove a = do s1 <- readIORef r r' <- newIORef s1 x <- a s3 <- readIORef r' writeIORef r s3 return x and this goes through w/o problems, as I can now safely move the first two lines past the x <- a. Thanks for all the help. Ben