[Haskell-cafe] Re: Proving stuff about IORefs

[Ben Franksen]

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