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 q2N6k2P0011501 for ; Fri, 23 Mar 2012 07:46:02 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0EAAobbE+FBoIF/2dsb2JhbABEuG2CCQEBBAEnEwYDATUBAQMLCzQSVwYuh2oEpSyEM44wAQaQIGOIWI0LkCiCdg X-IronPort-AV: E=Sophos;i="4.73,634,1325458800"; d="scan'208";a="150831902" 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; 23 Mar 2012 07:45:55 +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 899A962C6; Fri, 23 Mar 2012 15:45:52 +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 5393539A3; Fri, 23 Mar 2012 15:45:52 +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=enxJRk4cLh/MGknXDvFMGcLo/YM=; b=b8HxujaSForGVOOFLN1SI0Zhsg94 cJpzn1L11JnndoPvWQ63F/awfv2h+eWLUy/bsSr1HWeYKFoNCog56+jNMbfYQbuY E8uXKrWcuIvk8u2CjlDIwDox/HCF6EPROrOkOY1lOPTAtq9g0VAdCPmTcKyNDBou 7SkAaAP6Mpp2/b8= 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=RBVpXTRL2HFPCYv3aYBL7B3f3DjJxs0D0anGMYTq4NcG4XfTC5rTTSDXGWz4EIf+DbPGFMkKoM73IjuhlVE7rww9XCI4hkt0YH3yLU2VLo4gLKLAyuA56GuKjEXGWHQkUtrhmZEZLd4b/jPyQaZcymg2KteloE4vhORV4JhBtio=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 042CD39A2; Fri, 23 Mar 2012 15:45:51 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Fri, 23 Mar 2012 15:45:51 +0900 Cc: Roberto Di Cosmo , caml-list@inria.fr Message-Id: <8F5F6351-7DF3-4BFD-BE79-6B76696A457C@math.nagoya-u.ac.jp> References: <20120322095143.GA30016@voyager> To: Gabriel Scherer X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q2N6k2P0011501 Subject: Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS? On 2012/03/23, at 14:52, Gabriel Scherer wrote: >> 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. > > I'd rather use a warning here. There are enough subtleties with (type > a b . foo) already, I possible I would be glad not to have to explain > different scoping rules from the rest of the language. The point here is that the "type a b. ..." syntax is syntactic sugar. Rather than putting efforts in making it "hygienic", at the cost of mangling type variable names, isn't it simpler to define precisely how it expands, and prohibit ambiguous types? I would argue that this is actually simpler to explain it that way (if you want to give an exact specification). I have committed this in trunk and 4.00, and the output now is a syntax error: Error: In this scoped type, variable 'a is reserved for the local type a. It is of course possible to make it a warning (by doing two passes and generating fresh names), but I don't see the point: you can always choose your names so that no conflict happens, so why risk the confusion? A similar case occurs with value fields in classes: not only you cannot access them from other value fields, but they actually hide external values. >> 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. > > That would be quite strange. I already find it dubious that (type a b > . ....) would escape its natural scope, but our nice old type > variables had not been affected by those changes yet, and I think it's > better that they keep their natural meaning of local quantification. Backward compatibility is of course a concern. On the other hand, polymorphic methods are not used that often, and problems only occur with code that is ambiguous to read. For me the main problem is that it hides the fact those type variables are really locally abstract types. And the idea behind using locally abstract types was to avoid introducing yet another kind of type variable. > Could we get the type-checker to understand that > let rec length (type a) (type b) : (a, b) l -> _ = function ... > or let rec length (type a) (type b) (li : (a, b) l) = ... > is polymorphic enough to be a case of polymorphic recursion? This way > we could get rid of the (type a b . ....) syntax altogether have > clearer scoping rules. This is certainly doable, but in my opinion it would not replace the "type a b. ..." syntax, which is more readable. > (On my wishlist: ... (type a) (type b) ... could be written ... > (type a b) ...) Easy to do. Actually I'm not sure why it wasn't defined that way to start with. Not enough System F-ish? Jacques Garrigue