From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=-0.0 required=5.0 tests=NO_RELAYS autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: by yquem.inria.fr (Postfix, from userid 18041) id 0BB6ABC69; Thu, 8 Feb 2007 20:08:44 +0100 (CET) Date: Thu, 8 Feb 2007 20:08:44 +0100 To: David Allsopp Cc: OCaml List Subject: Re: [Caml-list] More intelligent match warnings Message-ID: <20070208190844.GA26988@yquem.inria.fr> References: <005501c74bab$369f5150$6a7ba8c0@treble> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <005501c74bab$369f5150$6a7ba8c0@treble> User-Agent: Mutt/1.5.9i From: maranget@yquem.inria.fr (Luc Maranget) X-Spam: no; 0.00; maranget:01 maranget:01 compiler:01 emits:01 constructors:01 compiler:01 decidable:01 computations:01 decidable:01 compilation:01 compilation:01 mutable:01 statically:01 doable:01 matchs:98 > Say I write the following rather pointless piece of code: > > type t = A | B | C > let f x = > match x with > A -> 1 > | _ -> match x with > B -> 2 > | C -> 3 > > The compiler emits Warning P for the second match because it's incomplete > over the constructors of type t. Indeed it does. > However, it's not really incomplete Well I guess that completeness is in the eye of the viewer, you and the compiler do not have the same eye. The compiler is shortsighted... > .. SNIP... < > > Are these two cases decidable in the general case? > What are you asking for exactly ? If you give one example of which all computations terminate well, exhautiveness is indeed decidable. More seriously, PM checks are performed independently, and at times sometimes quite unexpected, due to interaction with typing. It is a pity not to consider interaction beetween PM expressions. However consider that it makes the compiler simpler, safer and faster. More generally if you have match x with | p_1 -> ... | p_{n-1} -> .. | p_n ->HERE ... THERE Then, at point HERE (just after ->, we also assume no where clauses) we have some information about x : x does not match all the pattern [p_1 ; ... ; p_{n-1} ] x matchs the pattern p_n In your example we know that x does not match [A] and that it matches _ This information is complete for performing PM checks (and optimized compilation). In fact, warnings and compilation of one PM expression, compute and use exactly that information (compilation sometimes forget it for the sake of not having too big data structures). Later, at point THERE, well it depends, especially if matched x has mutable subcomponents. Now consider variations on your example (*1*) type t = A | B | C let f x = match x with A -> 1 | _ -> let y = x in match y with (* exhaustive *) B -> 2 | C -> 3 Of even worse (*2*) let f x = match x with A -> 1 | _ -> let y = match x with B -> C | C -> B in (* exhaustive *) match y with (* exhaustive *) B -> 2 | C -> 3 I guess (just a guess) that saved from running the program for all possible value, a compiler can decide statically that the matches are exhaustive. 1. Keep track of variable values (I mean associate pairs [p1.. pn-1], pn to variables), consider aliases. 2. Also consider information infeered from performing PM more involved but doable. a - since x is [A],_ the first match is exhaustive, one of the two clauses matches. b - The result is the union of [], C and [],B, that is [],(B|C) c - y is bound to [],(B|C) d - the second match is exhaustive. I am sure that implementing even 1, is a some amount of work, I am not sure that users would even notice the difference... > David > -- Luc Maranget