[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.
Regards,
Malcolm
More information about the Haskell-Cafe
mailing list