[Haskell-cafe] Re: Proving stuff about IORefs
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
>> 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
More information about the Haskell-Cafe
mailing list