From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 4072EBC8E for ; Wed, 16 Feb 2005 01:43:28 +0100 (CET) Received: from mail.davidb.org (adsl-64-172-240-129.dsl.sndg02.pacbell.net [64.172.240.129]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j1G0hQXc030464 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 16 Feb 2005 01:43:27 +0100 Received: from davidb by mail.davidb.org with local (Exim 4.43 #1 (Debian)) id 1D1DHo-0000Tk-PN; Tue, 15 Feb 2005 16:43:24 -0800 Date: Tue, 15 Feb 2005 16:43:24 -0800 From: David Brown To: Gilles Dubochet Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic variant typing Message-ID: <20050216004324.GA1537@old.davidb.org> References: <7bf1f3b95c18eeda0ed169eb7f73d6f0@urbanet.ch> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <7bf1f3b95c18eeda0ed169eb7f73d6f0@urbanet.ch> User-Agent: Mutt/1.5.6i X-Miltered: at concorde with ID 4212972E.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 caml-list:01 wrote:01 o'caml:01 wand:01 notation:01 notation:01 o'caml:01 int':01 intuitively:01 'x':01 statically:01 polymorphic:01 polymorphic:01 expression:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.9 required=5.0 tests=FORGED_RCVD_HELO,SPF_SOFTFAIL autolearn=disabled version=3.0.2 X-Spam-Level: On Tue, Feb 15, 2005 at 09:28:52PM +0000, Gilles Dubochet wrote: > Hello everyone, > > The following O'Caml expression: > let incr g x = match x with > | `Int i -> `Int (i+1) > | x -> (g x);; > > Receives type: > (([> `Int of int ] as 'a) -> ([> `Int of int ] as 'b)) -> 'a -> 'b > > Why? I am quite astonished. I would have expected a type more like: > ([> ] -> [> ]) -> [> `Int of int ] -> [> `Int of int ] > > or in Wand or Rémy-like row variable notation with which I am a little > more comfortable (I am not exactly sure the preceding type is correct > in the 'at leat - at most' notation of O'Caml): > ([ 'a ] -> [ 'b ]) -> [ `Int of int | 'a ] -> [ `Int of int | 'b ] > > Could anyone be kind enough to give me some clues about where to look > at to find an explanation or even better, explain me what is going on? > I am particularly puzzled by the fact that the g function's *argument* > type is 'at least `Int of int'. This rejects the following code which > seems intuitively correct: > incr (function `Float f -> `Float (f+.1.));; We know that 'incr' can take a [> `Int of int] for 'x', since it matches is. The only way to know that it isn't going to call 'g' with one of these would be to do a flow analysis of the code. The type system is not based on this type of analysis, but is determined statically. The polymorphic types are not really dynamic types. A particular type used in a given call will have a specific type, and in this instance, it must always contain [> `Int of int]. Dave