[Haskell-cafe] Re: Proving stuff about IORefs

[Ben Franksen]

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