From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 03F8EBC84 for ; Fri, 1 Apr 2005 18:26:26 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j31GQPeG012816 for ; Fri, 1 Apr 2005 18:26:25 +0200 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 SAA07952 for ; Fri, 1 Apr 2005 18:26:25 +0200 (MET DST) Received: from yquem.inria.fr (yquem.inria.fr [128.93.8.37]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j31GQ4eM014033; Fri, 1 Apr 2005 18:26:04 +0200 Received: by yquem.inria.fr (Postfix, from userid 18041) id 30E59BC84; Fri, 1 Apr 2005 18:26:04 +0200 (CEST) Date: Fri, 1 Apr 2005 18:26:04 +0200 To: Jacques Garrigue Cc: yminsky@cs.cornell.edu, yminsky@gmail.com, caml-list@inria.fr Subject: Re: [Caml-list] When is a function polymorphic? Message-ID: <20050401162604.GA24371@yquem.inria.fr> References: <891bd339050330165142478f37@mail.gmail.com> <20050331.114253.48852731.garrigue@math.nagoya-u.ac.jp> <891bd33905033020045cad3ce2@mail.gmail.com> <20050331.173223.128566586.garrigue@math.nagoya-u.ac.jp> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20050331.173223.128566586.garrigue@math.nagoya-u.ac.jp> User-Agent: Mutt/1.3.28i From: luc.maranget@inria.fr (Luc Maranget) X-Miltered: at nez-perce with ID 424D7631.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 424D761C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 luc:01 maranget:01 luc:01 maranget:01 yaron:01 minsky:01 yminsky:01 avoided:01 predictable:01 variants:01 variants:01 polymorphic:01 polymorphic:01 typing:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: > From: Yaron Minsky > > > Interesting. I guess this is best understood as a limitation of the > > type-checking algorithm. Does anyone know if there are any plans to > > remove this limitation? Are there fundamental reasons why it would be > > difficult to do so? > > This is not a limitation of the type checking algorithm per se. > Rather, the type checking algorithm prefers not to use > exhaustiveness information when this can be avoided, to keep it > predictable. > (Exhaustiveness is only used for polymorphic variants, but for > a deeper reason.) Besides, the test for exhautiveness much relies on typing having been performed. (Except for variants, which undergo a preliminary, specific kind of exhautiveness checking before typing). -- Luc Maranget