ndmitchell:
OK. i'm just trying to get an intuition for the analysis.
Catch is defined by a small Haskell program. You can write a small Haskell evaluation for a Core language. The idea is to write the QuickCheck style property, then proceed using Haskell style proof steps. The checker is recursive - it assigns a precondition to an expression based on the precondition of subexpressions, therefore I just induct upwards proving that each step is correct individually. There wasn't an intention of trying to move partiality around, but perhaps it has worked out that way.
What is the nature of the preconditions generated?
A precondition is a proposition of pairs of (expression, constraint), where an pair is satisfied if the expression satisfies the constraint. I prove that given a couple of lemmas about the constraint language, the analysis is correct. I then prove that 2 particular constraint languages have these necessary lemmas.
As a side note, I'm pretty certain that the constraint languages I give aren't the best choice. The second one (MP constraints) is good, but lacks an obvious normal form, which makes the fixed point stuff a little more fragile/slow. I'm sure someone could come up with something better, and providing it meets a few simple lemmas, it's suitable for Catch.
In order for them to cancel out the calls to error, are they constructed from information in the caller (as I speculated) about how the function under analysis is used?
Yes, information from case branches add to the constraint, so:
case xs of [] -> [] _:_ -> head xs
becomes: xs == [] \/ safe (head xs) xs == [] \/ xs == _:_ True
Obviously, you're also using a restricted notion of "bottom".
For my purposes, bottom = call to error. Things such as missing case branches and asserts are translated to error. I actually consider non-termination to be a safe outcome, for example Catch says:
assert (last xs) True
This is safe if all elements of the list are True (Catch approximates here), or if the list xs is infinite.
Thanks, that's helpful, and much what I expected. -- Don