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

[Luc Maranget <luc.maranget@inria.fr>]

> 
> 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.
The problem you refer is not related to the new pattern matching
compiler.

> 
> 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!


I decided not to flag a warning when all PM clauses have a ``when''
guard, assuming that programmers who use such a bad style
do not care about warnings.
(Note that such a  matching is considered non-exhaustive internally,
otherwise PM compilation would be broken).


Looking back on it, I see this is a mistake (Users care). I change it again,
this is a one minute fix, and I WILL NEVER CHANGE IT AGAIN.


> 
> 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>
> #
> 
I am glad that you do not notice that ``the value that is not
matched'' is indeed matched. (See at the end for an explanation)


> 
> 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 ! :-))
Nothing is said about computing exhaustiveness in the paper
(well almost nothing...)
Nothing is said on guards because guard compilation basically hasn't
changed and that there is a 12 pages limit.

> 
> Conclusion and personal opinion:
> 
> I think things changed between 3.00 and 3.02, no ?
Yes, but only for ``all when'' (and variants but there...).

> 
> If so, is this considered a bug ?
I consider this change as bad and reverse to the 3.00 behavior.

> 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.

Finally I talk a bit about unsused/exhautive checks in the presence
of when. As I agree with your point 3.
(Just saying ``nothing is guaranteed if you use ``when'', is not
enough).

Now (provided the special case for ``all when'' is removed), for
analysing PM, the compiler first supresses all guarded clauses, then
it analyses the resulting matching.

Thus,
  1. Provably unused guarded clauses are not detected.
     (Nobody has yet complained about that).
  2. Exhaustiveness check errs on the safe side.
  3. The ``non-matched'' value can be wrong, if at least one
     clause is guarded.

This can be corrected to some extend (err on the safe side,
give provably non matched values only), but this is more work for me,
and for the compiler.

I agree with all your comments, but I want to stress on the fact that
``when'' clauses are so called ``advanced features'', which should be
used only when it is not possible to express the same behavior more
simply.
As such, most examples given in such discussions are bad style anyway,
writting

match c with | (x,_) when x=0 -> ...

is not a good idea. And, as a teacher, I see  students do such
things.

My point is not ``garbage in'' ``garbage out'' (I am not that rude or
angry).
My point is:
If I were to demonstrate the power of OCaml to a friend,
I would  give an example where using a guarded pattern is justified,
such as

(* checks that x is some zero)
match x with
| Some 0 -> true
| _      -> false
n
(* checks that x is some even value *)
match x with
| Some x when x mod 2 = 0 -> true
| _ -> false

(* Borderline case *)
match x with
| Some x when x mod 2 = 0 -> "even"
| Some x when x mod 2 = 1 -> "odd"

No warning! Bad, the caml team will correct it now!

But notice that the following match gives a warning.
match x with
| Some x when x mod 2 = 0 -> "even"
| Some x when x mod 2 = 1 -> "odd"
| None -> "nothing"
Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Some _


Given the behavior of the PM analyser
this  should probably has been written as

match x with
| Some x when x mod 2 = 0 -> "even"
| Some _ -> "not even (I mean odd)"
| None -> "nothing"


Notice that things are not perfect still for another reason

match x with
| Some _ -> "not even (I mean odd)"
| Some x when x mod 2 = 0 -> "even" 
| None -> "nothing"

There is no warning for the unused clause number 2.

> 
> Have a nice day, OCamlers!
> 
> Jean-Marc Eber
> LexiFi Technologies
> 
Thanks you for you remarks (I mean it!).

--Luc


-------------------
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