[Haskell-cafe] Re: Proving stuff about IORefs

17 Oct 2010

      Derek Elkins wrote:
...
On Sat, Oct 16, 2010 at 9:21 PM, Ben Franksen 
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