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

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
return (x, s')
callback action r = do
(x, s') <- runStateT (unStateIO action) s
writeIORef r s'
return x

The original idea comes from this message

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
return (x, s4)
= { def callback }
StateIO \$ StateT \$ \s1 -> do
r <- newIORef s1
x <- do
(x, s3) <- runStateT (unStateIO o) s2
writeIORef r s3
return x
return (x, s4)
StateIO \$ StateT \$ \s1 -> do
r <- newIORef s1
(x, s3) <- runStateT (unStateIO o) s2
writeIORef r s3
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)
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
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
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
(x, s4) <- runStateT (unStateIO (embed f)) s1
writeIORef r s4
return x
= { def embed }
do
(x, s4) <- runStateT (unStateIO \$ StateIO \$ StateT \$ \s2 -> do
r' <- newIORef s2
x <- f r'
return (x, s3)
) s1
writeIORef r s4
return x
= { def StateIO, StateT, beta reduce }
do
(x, s4) <- do
r' <- newIORef s1
x <- f r'
return (x, s3)
writeIORef r s4
return x
do
r' <- newIORef s1
x <- f r'
writeIORef r s3
return x
= { IORef laws }
do
r' <- newIORef s1
x <- f 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

```