[Caml-list] Pattern matcher no more supposed to warn on non exhaustive patterns ?

["Jean-Marc Eber" <jeanmarc.eber@lexifi.com>]

Dear OCamlers,

I don't know if the following is a bug, but it seems contrary to what
I understood from a few postings on this list. I also suspect a
(profound) modification introduced by the "new pattern matching
compiler". This modification doesn't seem (to me at least) to have
been documented somewhere.

Last Sunday, a former colleague visited me. I wanted to convince him
about the advantage of functional programming over other approaches,
when using a powerful compiler. I began with pattern matching and
exhaustiveness analysis/warnings, showing him how the compiler may
spot to the programmer some "forgotten" cases.



        Objective Caml version 3.02

# let f = function
  | 0, _ -> 1
  | _, 0 -> 2;;
Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(1, 1)
val f : int * int -> int = <fun>
#

OK, thats fine, and we are happy: of course, we didn't "cover the
board", and treated only some particular cases!

Now lets do it with guarded patterns:

# let f = function
  | x, _ when x=0 -> 1
  | _, y when y=0 -> 2;;
val f : int * int -> int = <fun>
#

OOPS: no more non-exhaustiveness warning!
I understand well of course that the compiler isn't able to do an
analysis of the expression in a when clause, but thought that because
of this impossibility, the compiler supposed, for exhaustiveness
analysis, that a when clause would "always be false", assuming that
this branch would not be taken. This clearly isn't the case here!

Now suppose that we "extend" a little bit function f and treat some
more cases:

# let f = function
  | x, _ when x=0 -> 1
  | _, y when y=0 -> 2
  |1, _ -> 3;;
Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(0, _)
val f : int * int -> int = <fun>
#

So by *adding* a clause to the pattern matcher we "transformed" a
function without warning in a function (now correctly) spotting some
incompleteness. The exhaustiveness analyzer is no more *monotonic*, a
property one would intuitively assume.

I always thought that by making the "pessimistic" assumption about
guarded patterns, we had the following theorem: a program compiling
without exhaustiveness warning can never raise a Match_failure
exception. This is of course a very nice static property, and I always
programmed (by, in some rare cases, adding a "dummy" case I knew would
never been taken, but making the exhaustiveness analyzer happy) in
this way. This theorem is LOST!

I looked at Le Fessant's and Maranget's ICFP 2001 paper, but if I'm
not wrong, it doesn't treat the guarded pattern case (a case of non
exhaustiveness indeed, so we don't know if the OCaml derived "paper
content compiler" would warn about it ! :-))

Conclusion and personal opinion:

I think things changed between 3.00 and 3.02, no ?

If so, is this considered a bug ?

my opinion:
1. loosing any kind of static property theorem is TERRIBLE and should
be avoided if possible!
2. exhaustiveness analysis is a "big deal" for practical programming
work. In some complex datastructures, it really helps you track down
some errors in algorithms.
3. (well used) guarded patterns (when clause) are often very useful
(expressions would sometimes become much more complex without them!)
and their use should not be discouraged by poor exhautivenss analysis.

Have a nice day, OCamlers!

Jean-Marc Eber
LexiFi Technologies




-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr