[Haskell-cafe] Re: Proving stuff about IORefs

Malcolm Wallace malcolm.wallace at me.com
Sun Oct 17 06:15:39 EDT 2010

>>> 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?

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.


More information about the Haskell-Cafe mailing list