Re: Irrelevant variables in patterns

[John Harrison <John.Harrison@cl.cam.ac.uk>]

Chet writes:

| Exceptions in ML are a programming mechanism.  They are not used
| anymore for exceptional conditions.  We need a new mechanism for that.

In the HOL theorem prover we use exceptions to indicate that certain
inference rules are inapplicable. It's quite common for code to trap
failures at certain subterms and conclude "we have rewritten this subterm
as much as possible, so return it". In the present code (including hol90 in
SML) most of the exceptions are caught completely indiscriminately, i.e.
`_' not `HOL_ERR(_)'. This means there are situations where exceptional
conditions just get driven over. Really the code should be rewritten, but
as Chet remarks, there's something to be said for a separate signal
mechanism.

| Moreover, even if I _do_ write the code in handle_exceptions_generally
| to treat Out_of_memory, etc, I get many warnings telling me that I am
| catching the exception.

Which raises another point. Is there a way to suppress the incredibly
irritating (and I seem to recall not very accurate) "match not exhaustive"
messages in CAML Light (in general expression matching as well as
exceptions)? I find myself putting in redundant clauses to avoid them,
which is hardly good style. It's especially pointless when the match is
actually done at toplevel, e.g.

  let [x;y] = [1;2];;

As Christophe says:

|                               [...] Then what you really needs is a compiler
| option to discard a particular warning (or class or warning) so you only get
| the warnings which are relevant to you programming style.

I agree completely.

John.