[Haskell-cafe] Re: Proving stuff about IORefs
Ben Franksen
ben.franksen at online.de
Sun Oct 17 00:16:51 EDT 2010
Derek Elkins wrote:
> On Sat, Oct 16, 2010 at 9:21 PM, Ben Franksen <ben.franksen at online.de>
> wrote:
>> I have a formal proof where I am stuck at a certain point.
>>
>> 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
>>
>> What happens here is that the temporary IORef r' takes the place of the
>> argument r, and after we apply f to it we take its content and store it
>> in the original r. This should be the same as using r as argument to f in
>> the first place.
>>
>> How can I prove this formally?
>
> You haven't provided us with any information about the formal model
> you are using and your question is somewhat ambiguously phrased, hence
> Thomas' response where, I'm pretty sure, he misunderstood what you
> were asking.
I don't have a model. Up to this point I can make do with equational
reasoning.
This is the context. I have this class
class Embed i o where
type Content i o
embed :: (Content i o -> i a) -> o a
callback :: o a -> Content i o -> i a
which I _think_ should have these laws attached
L1: embed . callback == id
L2: callback . embed == id
and an instance
newtype StateIO s a = StateIO { unStateIO :: StateT s IO a }
instance Embed IO (StateIO s) where
type Content IO (StateIO s) = IORef s
embed f = StateIO $ StateT $ \s -> do
r <- newIORef s
x <- f r
s' <- readIORef r
return (x, s')
callback action r = do
s <- readIORef r
(x, s') <- runStateT (unStateIO action) s
writeIORef r s'
return x
The original idea comes from this message
http://www.haskell.org/pipermail/haskell-cafe/2007-July/028501.html
but I have deviated somewhat from Jules' notation and generalised.
Now I want to prove the laws. L1 is straight forward:
embed (callback o)
= { def embed }
StateIO $ StateT $ \s1 -> do
r <- newIORef s1
x <- callback o r
s4 <- readIORef r
return (x, s4)
= { def callback }
StateIO $ StateT $ \s1 -> do
r <- newIORef s1
x <- do
s2 <- readIORef r
(x, s3) <- runStateT (unStateIO o) s2
writeIORef r s3
return x
s4 <- readIORef r
return (x, s4)
= { Monad laws }
StateIO $ StateT $ \s1 -> do
r <- newIORef s1
s2 <- readIORef r
(x, s3) <- runStateT (unStateIO o) s2
writeIORef r s3
s4 <- readIORef r
return (x, s4)
= { IORef laws }
StateIO $ StateT $ \s1 -> do
r <- newIORef s1
(x, s3) <- runStateT (unStateIO o) s1
writeIORef r s3
return (x, s3)
= { reorder (r is unused in second stmt), Monad laws }
StateIO $ StateT $ \s1 -> do
(x, s3) <- runStateT (unStateIO o) s1
r <- newIORef s1
writeIORef r s3
return (x, s3)
= { IORef laws }
StateIO $ StateT $ \s1 -> do
(x, s3) <- runStateT (unStateIO o) s1
return (x, s3)
= { Monad laws }
StateIO $ StateT $ \s1 -> runStateT (unStateIO o) s1
= {def StateIO, StateT }
o
You might question the step marked { IORef laws }. I don't know if this has
been formalized anywhere but I thought it safe to assume a law that states
do
r <- newIORef a
b <- readIORef r
g b
=
do
r <- newIORef a
g a
assuming that a is not used any further.
Similarly I have used the "law"
do
writeIORef r a
b <- readIORef r
g b
=
do
writeIORef r a
g a
Both of these are so obviously satisfied that I accept them as axioms.
Now, when I try to prove L2, I can reason similarly and get
callback (embed f) r
= { def callback }
do
s1 <- readIORef r
(x, s4) <- runStateT (unStateIO (embed f)) s1
writeIORef r s4
return x
= { def embed }
do
s1 <- readIORef r
(x, s4) <- runStateT (unStateIO $ StateIO $ StateT $ \s2 -> do
r' <- newIORef s2
x <- f r'
s3 <- readIORef r'
return (x, s3)
) s1
writeIORef r s4
return x
= { def StateIO, StateT, beta reduce }
do
s1 <- readIORef r
(x, s4) <- do
r' <- newIORef s1
x <- f r'
s3 <- readIORef r'
return (x, s3)
writeIORef r s4
return x
= { Monad laws }
do
s1 <- readIORef r
r' <- newIORef s1
x <- f r'
s3 <- readIORef r'
writeIORef r s3
return x
= { IORef laws }
do
s1 <- readIORef r
r' <- newIORef s1
x <- f r'
s3 <- readIORef r'
writeIORef r s3
return x
= { ??? }
f r
and I would like to reduce the last step to the same level of "obviosity" as
in the previous proof.
> At any rate, if you intend to prove this for any arbitrary f, I can't
> tell you how to prove it formally because it's not true.
How do you know that? Can you give an example where it fails?
Cheers
Ben
More information about the Haskell-Cafe
mailing list