Ben Franksen ben.franksen at online.de
Sun Oct 17 20:55:10 EDT 2010

```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
>>     r' <- newIORef s1
>>     x <- f 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
r' <- newIORef s1
x <- a
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

```