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

[Pierre Weis <pierre.weis@inria.fr>]

> So long as the issue of when clauses has come up, I'll also point out that
> the pattern-compiler essentially assumes that when clauses are pure.  I'm
> not complaining because I consider it poor style to violate this assumption,
> but I've never heard it discussed anywhere.
> 
> For the program below, ocamlopt version 3.00 produces a program that prints
> 1314.
> 
> --Dan
> 
> -- 
> | Dan Grossman     www.cs.cornell.edu/home/danieljg H:607 256 0724 |
> | 5157 Upson Hall  danieljg@cs.cornell.edu          O:607 255 9834 |
[...]

I'm not sure that the pattern-matching compiler has something to
assume about guards except that they return a boolean.

Anyway, I presume that the programmer who reads your program
intuitively assumes the purity of the guards, so that you're
absolutely right:
``it is poor style to violate this assumption''.

Concerning the documentation, and even if the Caml FAQ does not
explicitely states that guards (or when clauses) should be pure, it
explains in details the related problem of partial matches in the
presence of guarded clauses; as a counter-example, we used guards with
side-effects, and we note how complex the semantics can be in those
cases:

let rec f = function
 | n when g (n + 1) >= 0 -> n
 | n when g (n + 1) < 0 -> n + 1

and g =
 let alea = ref true in
 (function n ->
    alea := not !alea;
    if !alea then -1 else 1);;

This example shows why a guard should always be considered as possibly
false (the usual semantics that Jean-Marc promoted in his post), since
even if the guards here are synctactically of the form ``when cond''
and ``when not cond'', they are not opposite and the pattern matching
is definitively not exhaustive (in fact, f almost always fails!).

Admittedly, we must add in the FAQ an explicit warning to the
programmer that using side-effects into guards is a very bad
practice. On the other hand, the compiler would be right to consider
guarded clauses as possibly false and emit a warning when patterns are
not exhaustively covered by other non guarded clauses (as a
refinement, the warning could be a ``POSSIBLY not exhaustive match''
warning, if the pattern that is not covered was matched by a when
clause). Otherwise, the naive reader of the code of the function f
above would be erroneously conforted by the Caml compiler that f is
total when it is certainly not!

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/


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