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

On Sun, Oct 17, 2010 at 11:15 AM, Malcolm Wallace wrote:

The problem with the code you originally posted was that it looked like this:

 f r = do r' <- something           f r'           something else -- this is dead code

That is, the computation is non-terminating, because f simply calls itself recursively, with no base case.

Regards,    Malcolm

He was using ==, not =, it was a statement of equality not a definition :) Much like one might say that sort xs == sort (reverse xs).

Derek Elkins wrote:

On Sun, Oct 17, 2010 at 6:49 AM, Miguel Mitrofanov wrote:

...

On 17 Oct 2010, at 05:21, Ben Franksen wrote:

...

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

That is not true. Consider the following function:

g r1 r2 = writeIORef r1 0 >> writeIORef r2 1 >> readIORef r1

This function behaves differently depending on whether r1 and r2 are the same IORef or not. Therefore, the property you want to prove doesn't hold for the partially-applied function

f = g r1

I originally was thinking along these lines, and this is an important case, but there is an even more trivial example.

Let f be return.

Oh, my god. Of course. Thanks for pointing me to the obvious ;-) This means I either have to give up on the second law callback . embed = id or find another implementation. Maybe IORef is too powerful. Hmm. The second law was inspired by the instance for ReaderT: instance Embed m (ReaderT r m) where type Content m (ReaderT r m) = r embed = ReaderT callback = runReaderT which is much more general (it does not depend on the inner monad being IO), and where indeed the second law holds. Cheers Ben

Hi Mathew Matthew Brecknell wrote:

Ben Franksen wrote:

...

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

I'm not sure where in your question the quantifiers for types a and b are intended to be.

If you really do mean:

"Given an arbitrary function f with polymorphic type f :: forall a b. IORef a -> IO b prove that..."

then you might be able to appeal to parametricity. I wouldn't know how to apply parametricity to IO actions, though.

No, I would have written this explicitly as f :: forall a b. IORef a -> IO b . I thought it is the generally accepted convention that free variables appearing in a proposition are understood to be universally quantified (at the outermost level). If we had to always explicitly write down all the quantifiers, formulas would quickly become unwieldy.

On the other hand, Miguel and Derek seem to be interpreting these as meta-variables which are quantified over the whole question; in other words, that you mean:

"Given arbitrary types A and B, and a function f :: IORef A -> IO B prove that..."

Derek's counter-example is then, more explicitly:

type A = () type B = IORef () f = return

If I had time to digest your second post, I might be able to figure out which of these (plus a couple of other possibilities) is required. So my point is just that if you don't think about these things explicitly, it's easy to unwittingly make an assumption, possibly to the detriment of whatever you're trying to achieve.

Right, in general. That wasn't my mistake, though. I just wanted the law to hold so badly I forgot that IORefs have an identity separate from what their content is, so even if what the do-block returns has the same content, it is still a different IORef. However, I have the notion now that it suffices to prove something much weaker, namely callback . embed . const = id Note that this is a special case of the original law callback . embed = id It means that the IO action does not get passed a reference and thus I need only prove a = do s1 <- readIORef r r' <- newIORef s1 x <- a s3 <- readIORef r' writeIORef r s3 return x and this goes through w/o problems, as I can now safely move the first two lines past the x <- a. Thanks for all the help. Ben