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 SAA24030; Wed, 3 Oct 2001 18:08:20 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA24026 for ; Wed, 3 Oct 2001 18:08:20 +0200 (MET DST) Received: from postfix2-2.free.fr (postfix2-2.free.fr [213.228.0.140]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f93G8Jf07381 for ; Wed, 3 Oct 2001 18:08:19 +0200 (MET DST) Received: from N7YYB (nas-cbv-2-30-163.dial.proxad.net [213.228.30.163]) by postfix2-2.free.fr (Postfix) with SMTP id 1A63C5FB56 for ; Wed, 3 Oct 2001 18:08:18 +0200 (CEST) Message-ID: <007201c14c32$37e4c5a0$060000c0@N7YYB> From: "Jean-Marc Eber" To: "caml-list" Subject: [Caml-list] Pattern matcher no more supposed to warn on non exhaustive patterns ? Date: Wed, 3 Oct 2001 19:37:56 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="EUC-KR" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 4.72.3155.0 X-MimeOLE: Produced By Microsoft MimeOLE V4.72.3155.0 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. 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 = # 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 = # 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 = # 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