From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA11472; Thu, 4 Oct 2001 09:55:54 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA11407 for ; Thu, 4 Oct 2001 09:55:54 +0200 (MET DST) Received: from beaune.inria.fr (beaune.inria.fr [128.93.8.3]) by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id f947trP19887 for ; Thu, 4 Oct 2001 09:55:53 +0200 (MET DST) Received: by beaune.inria.fr (8.8.8/1.1.22.3/14Sep99-0328PM) id JAA0000000512; Thu, 4 Oct 2001 09:55:52 +0200 (MET DST) From: Luc Maranget Message-Id: <200110040755.JAA0000000512@beaune.inria.fr> Subject: Re: [Caml-list] Pattern matcher no more supposed to warn on non exhaustive patterns ? To: jeanmarc.eber@lexifi.com (Jean-Marc Eber) Date: Thu, 4 Oct 2001 09:55:52 +0200 (MET DST) Cc: caml-list@inria.fr (caml-list) In-Reply-To: <007201c14c32$37e4c5a0$060000c0@N7YYB> from "Jean-Marc Eber" at oct 03, 2001 07:37:56 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > > 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 = > # > > 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 = > # > 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