Derek Elkins wrote:
> On Sat, Oct 16, 2010 at 9:21 PM, Ben Franksen <[email protected]>
> 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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
