From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2MMDKtM024033 for ; Thu, 22 Mar 2012 23:13:20 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj8HAFWja0+FBoIF/2dsb2JhbABEgw61NoIJAQEEAScTBgMBNQEBAwsLRlcGLodqBKU1hDOONQEGkAFjiFiNC4VtijuCdg X-IronPort-AV: E=Sophos;i="4.73,633,1325458800"; d="scan'208";a="150799049" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 22 Mar 2012 23:13:02 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8BBD262BF; Fri, 23 Mar 2012 07:12:54 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 558F239A2; Fri, 23 Mar 2012 07:12:54 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=I7EiLUKDFLzzbWr3iZ7SyehTgsQ=; b=f3VgEtmpCv0jAwXT2egMTkLHoPMV o6T3sTGyhzTlI9xQXcUP04WEQ9jbaMZcU0cmMmlqMEno+jKpyIUIKR+Way8Bi7u5 g3KcItGpifLrUpIOQdO9Iq9NIwITWn9Yb/BESCut7oauvcu4LulwihXOmGciJG3u I2IR7A0ZJlIVx4E= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=AZwrW4ds23qNIIx5N8lOGCn1b6JEGMt4lDtAZA1Biigg1hbMISSSq7/FXi6w+64qkjZ2OY00EFy0R2096Otf+Lp9LYzyAb/weS/dlSSD+j9Fucb2K9R9ovV8Ix/FBKOx4gMb39FHk7BTKNHz8Hceu0OFzeJLCp9NJthEKYpbTjc=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from [192.168.0.16] (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 07CD13998; Fri, 23 Mar 2012 07:12:54 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <20120322095143.GA30016@voyager> Date: Fri, 23 Mar 2012 07:12:52 +0900 Cc: caml-list@inria.fr Message-Id: References: <20120322095143.GA30016@voyager> To: Roberto Di Cosmo X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q2MMDKtM024033 Subject: Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS? On 2012/03/22, at 18:51, Roberto Di Cosmo wrote: > I was playing around some more with GADTs, preparing my next course > on functional programming, and came across an example on > which the type checker outputs a type containing a funny name > for a type variable. Dear Roberto, Thanks for testing the new features. There certainly are some rough edges left. > I do not know if this qualifies as a bug, so before filing it, I'd > love some feedback. > > Here we are: I am writing an example to show how one can code > a well typed length function for empty/nonempty list; we start > with the type definition > > type empty > type nonempty > > type ('a, 'b) l = > Nil : (empty, 'b) l > | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;; > > then we move on to the length function > > let rec length : type a b. (a,b) l -> 'a = function > | Nil -> 0 > | (Cons (_,r)) -> 1+ (length r);; > > Hey, you say, the natural type to declare for length should be > > type a b. (a,b) l -> int > > but as you see, for some mysterious reason I ended > up writing something silly (dont ask why, I am just > very well known to step on strange bugs as easily > as I breath) > > type a b. (a,b) l -> 'a > > The type checker is happy anyway: 'a will be instantiated > to int, and the declaration of length is accepted... but now > look at the output type > > val length : ('a1, 'b) l -> int = > > Why do we get 'a1, and not 'a, in the type? > > Well, probably, since 'a is instantiated to int during > type checking, it may be the case that 'a, as type name, is > still marked as taken during the type output, so we get ('a1,'b) > > The type is perfectly sound... it is just 'surprising' for > a regular user... do you think this should be considered a bug? Well, since there is no specification whatsoever about type variable names in the output, this is hard to call it a bug. On the other hand, you were surprised, so something is probably wrong. After thinking a bit more about it, actually the problem is not in the printer, as everybody assumed, but in the parser. Namely, ... : type a b. (a,b) l -> 'a = ... is just syntactic sugar for ... : 'a1 'b. ('a1,'b) l -> 'a = fun (type a) (type b) -> (... : (a,b) l -> 'a) Now you see where 'a1 appears: since there is already an 'a in the type, we cannot use 'a for the fresh abstract type a. However, as you already mentioned, the original type itself was erroneous. So a better solution would be to get an error at that point. Namely, if the type annotation contains a type variable with the same name as one of the quantified types. Does it sound reasonable. At times I wonder whether the "type a b. ...." syntax is the right approach. Another approach would be to change the meaning of ... : 'a 'b. ('a,'b) l -> 'a = ... to have 'a and 'b defined in the right hand side. The trouble is that we still need the locally abstract types internally, so this could be confusing. Also this could break some existing programs using polymorphic methods. Jacques Garrigue