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

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

[Dan Grossman]

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 |

===============

type y = {mutable c:bool}
type x = {a:y; b:y}

let f1 (v:x) = 
  match v with
    {a = _; b = _} when (v.a.c <- false; v.b.c <- false; false) -> 0
  | {a = {c=false}; b = {c=false}} -> 1
  | {a = {c=false}; b = {c=true}}  -> 2
  | {a = {c=true};  b = {c=false}} -> 3
  | {a = {c=true};  b = {c=true}}  -> 4

let f2 (v:x) = 
  match v with
    {a = {c=true}; b = _} when (v.a.c <- false; v.b.c <- false; false) -> 0
  | {a = {c=false}; b = {c=false}} -> 1
  | {a = {c=false}; b = {c=true}}  -> 2
  | {a = {c=true};  b = {c=false}} -> 3
  | {a = {c=true};  b = {c=true}}  -> 4

let f3 (v:x) = 
  match v with
    {a = _; b = {c=true}} when (v.a.c <- false; v.b.c <- false; false) -> 0
  | {a = {c=false}; b = {c=false}} -> 1
  | {a = {c=false}; b = {c=true}}  -> 2
  | {a = {c=true};  b = {c=false}} -> 3
  | {a = {c=true};  b = {c=true}}  -> 4

let f4 (v:x) = 
  match v with
    {a = {c=true}; b={c=true}} when (v.a.c <- false; v.b.c <- false; false)
-> 0
  | {a = {c=false}; b = {c=false}} -> 1
  | {a = {c=false}; b = {c=true}}  -> 2
  | {a = {c=true};  b = {c=false}} -> 3
  | {a = {c=true};  b = {c=true}}  -> 4

let main () =
  let v1:x = {a = {c=true}; b = {c=true}} in
  let v2:x = {a = {c=true}; b = {c=true}} in
  let v3:x = {a = {c=true}; b = {c=true}} in
  let v4:x = {a = {c=true}; b = {c=true}} in
  print_int (f1 v1);
  print_int (f2 v2);
  print_int (f3 v3);
  print_int (f4 v4)

let _ = main ()
-------------------
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

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

[Jean-Marc Eber]

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

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

[Luc Maranget]

> 
> 
> So long as the issue of when clauses has come up,
Well I am thinking about it, others complain loudly.



> 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,
You bet.
> 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 |

Argl....

Dear Dan, which result would you consider to be correct ?
(1111 ?)
Please tell me...
(Note that I see no consitency either in 3.02 or 3.00,)

Cheers, thanks,  and argl again !

--Luc

It is worth a warning in the manual, at least...

> 
> ===============
> 
> type y = {mutable c:bool}
> type x = {a:y; b:y}
> 
> let f1 (v:x) = 
>   match v with
>     {a = _; b = _} when (v.a.c <- false; v.b.c <- false; false) -> 0
>   | {a = {c=false}; b = {c=false}} -> 1
>   | {a = {c=false}; b = {c=true}}  -> 2
>   | {a = {c=true};  b = {c=false}} -> 3
>   | {a = {c=true};  b = {c=true}}  -> 4
> 
> let f2 (v:x) = 
>   match v with
>     {a = {c=true}; b = _} when (v.a.c <- false; v.b.c <- false; false) -> 0
>   | {a = {c=false}; b = {c=false}} -> 1
>   | {a = {c=false}; b = {c=true}}  -> 2
>   | {a = {c=true};  b = {c=false}} -> 3
>   | {a = {c=true};  b = {c=true}}  -> 4
> 
> let f3 (v:x) = 
>   match v with
>     {a = _; b = {c=true}} when (v.a.c <- false; v.b.c <- false; false) -> 0
>   | {a = {c=false}; b = {c=false}} -> 1
>   | {a = {c=false}; b = {c=true}}  -> 2
>   | {a = {c=true};  b = {c=false}} -> 3
>   | {a = {c=true};  b = {c=true}}  -> 4
> 
> let f4 (v:x) = 
>   match v with
>     {a = {c=true}; b={c=true}} when (v.a.c <- false; v.b.c <- false; false)
> -> 0
>   | {a = {c=false}; b = {c=false}} -> 1
>   | {a = {c=false}; b = {c=true}}  -> 2
>   | {a = {c=true};  b = {c=false}} -> 3
>   | {a = {c=true};  b = {c=true}}  -> 4
> 
> let main () =
>   let v1:x = {a = {c=true}; b = {c=true}} in
>   let v2:x = {a = {c=true}; b = {c=true}} in
>   let v3:x = {a = {c=true}; b = {c=true}} in
>   let v4:x = {a = {c=true}; b = {c=true}} in
>   print_int (f1 v1);
>   print_int (f2 v2);
>   print_int (f3 v3);
>   print_int (f4 v4)
> 
> let _ = main ()
> -------------------
> 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
> 

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

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

[Dan Grossman]

Luc Maranget wrote:
 
> Argl....
> 
> Dear Dan, which result would you consider to be correct ?
> (1111 ?)
> Please tell me...
> (Note that I see no consitency either in 3.02 or 3.00,)
> 
> Cheers, thanks,  and argl again !
> 
> --Luc

If this problem is worth fixing, I suggest that only 1111 or 4444 are
reasonable answers.  I tend to prefer 1111.  For fixing the
exhaustiveness-checker and pattern-compiler, it's probably easiest to do the
most expensive thing: the presence of a when clause basically invalidates
the failure of all previous cases -- it's like they weren't there.

Note that no change needs to be made except when the pattern's type includes
a mutable field.

Further note that threads are even harder to deal with -- they effectively
can put evil when clauses everywhere.  My familiarity with the ocaml
run-time is rusty, but perhaps a pattern-match (where the pattern's type
includes a mutable field) could be "rolled back" when the thread is
restarted.  Of course, you can't re-execute any when clauses! :-)

--Dan

> 
> It is worth a warning in the manual, at least...
> 
> >
> > ===============
> >
> > type y = {mutable c:bool}
> > type x = {a:y; b:y}
> >
> > let f1 (v:x) =
> >   match v with
> >     {a = _; b = _} when (v.a.c <- false; v.b.c <- false; false) -> 0
> >   | {a = {c=false}; b = {c=false}} -> 1
> >   | {a = {c=false}; b = {c=true}}  -> 2
> >   | {a = {c=true};  b = {c=false}} -> 3
> >   | {a = {c=true};  b = {c=true}}  -> 4
> >
> > let f2 (v:x) =
> >   match v with
> >     {a = {c=true}; b = _} when (v.a.c <- false; v.b.c <- false; false) -> 0
> >   | {a = {c=false}; b = {c=false}} -> 1
> >   | {a = {c=false}; b = {c=true}}  -> 2
> >   | {a = {c=true};  b = {c=false}} -> 3
> >   | {a = {c=true};  b = {c=true}}  -> 4
> >
> > let f3 (v:x) =
> >   match v with
> >     {a = _; b = {c=true}} when (v.a.c <- false; v.b.c <- false; false) -> 0
> >   | {a = {c=false}; b = {c=false}} -> 1
> >   | {a = {c=false}; b = {c=true}}  -> 2
> >   | {a = {c=true};  b = {c=false}} -> 3
> >   | {a = {c=true};  b = {c=true}}  -> 4
> >
> > let f4 (v:x) =
> >   match v with
> >     {a = {c=true}; b={c=true}} when (v.a.c <- false; v.b.c <- false; false)
> > -> 0
> >   | {a = {c=false}; b = {c=false}} -> 1
> >   | {a = {c=false}; b = {c=true}}  -> 2
> >   | {a = {c=true};  b = {c=false}} -> 3
> >   | {a = {c=true};  b = {c=true}}  -> 4
> >
> > let main () =
> >   let v1:x = {a = {c=true}; b = {c=true}} in
> >   let v2:x = {a = {c=true}; b = {c=true}} in
> >   let v3:x = {a = {c=true}; b = {c=true}} in
> >   let v4:x = {a = {c=true}; b = {c=true}} in
> >   print_int (f1 v1);
> >   print_int (f2 v2);
> >   print_int (f3 v3);
> >   print_int (f4 v4)
> >
> > let _ = main ()
> > -------------------
> > 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
> >

-- 
| Dan Grossman     www.cs.cornell.edu/home/danieljg H:607 256 0724 |
| 5157 Upson Hall  danieljg@cs.cornell.edu          O:607 255 9834 |
-------------------
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

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

[Pierre Weis]

> 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

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

[Luc Maranget]

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

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

[Luc Maranget]

Hum I wrote too fast...


>>>>   1. Provably unused guarded clauses are not detected.
This is not excatly true, some are detected.



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

There is a warning for the unused clause number 2.

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