Should exhaustiveness testing be on by default?

[Neil Mitchell]

> 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

Neil