From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2NAQV2G019245 for ; Fri, 23 Mar 2012 11:26:31 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnYCAAJPbE/RVdK2kWdsb2JhbABEDrdhCCIBAQEBCQkNBxIpggkBAQEDARICExkBGw8OAQMBCwYFCw0uIgERAQUBHAYTGweHYwWacwqMFoJxhH4/iHYBBQuQeASVX45JPYNSOA X-IronPort-AV: E=Sophos;i="4.73,636,1325458800"; d="scan'208";a="137399632" Received: from mail-iy0-f182.google.com ([209.85.210.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 Mar 2012 11:26:24 +0100 Received: by mail-iy0-f182.google.com with SMTP id k25so7673531iah.27 for ; Fri, 23 Mar 2012 03:26:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=DWT8QMSD94ZXeYuAcCnvkhCVG/PHrlQ7e5LaezwLoZU=; b=XAhTHbfZuiXQq+n6bJeYgp8YjKYywBi37cBtTq282eeOTUaizCRZPkvIhHOz4vRmpj tiyOnaCAKKQmowxW0lYPMVg3mBP+LDK8txAdE4TgPG6gT0JMyzbWAdkLE4gUskyAr8up wOC8mBUKJVZy9N/RqulWdxHJGsXSuxCwcUQzQ++BtuNKSFU+mooeYlVa04lwuI8NJzaL 6wYPNOtsIixGeKixJQ4J2z7k/5bHF+Yn0rnlUZVYW3ajxgRmFHf4aNjVqLa2jE+k2wlq 5U7gKJlwuMcRMgaej6BMyOVssTcIfsCfolixSZyYPPOtDvVkBF5K7oEJ4b5zO0h8/zSc zd1A== Received: by 10.50.46.194 with SMTP id x2mr1424411igm.60.1332498384602; Fri, 23 Mar 2012 03:26:24 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.3.38 with HTTP; Fri, 23 Mar 2012 03:25:44 -0700 (PDT) In-Reply-To: <8F5F6351-7DF3-4BFD-BE79-6B76696A457C@math.nagoya-u.ac.jp> References: <20120322095143.GA30016@voyager> <8F5F6351-7DF3-4BFD-BE79-6B76696A457C@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Fri, 23 Mar 2012 11:25:44 +0100 Message-ID: To: Jacques Garrigue Cc: Roberto Di Cosmo , caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q2NAQV2G019245 Subject: Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS? > 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 agree that not having to deal with name shadowing makes the macro-expansion explanation simpler. Furthermore, treating this as an error instead of a warning also makes the implementation simpler, which is a point in favor of your change. I'm not totally convinced by the idea that "type a b . ..." won't cause trouble to users because it is syntactic sugar: 1. To explain it directly as syntactic sugar, you have to explain the users both the polymorphic recursion notation and the rigid variable abstraction (type a) (is this a good name? I like "System F quantification" and prefer to avoid mumbles like "variables that are type constructors rather than type variables because of implementation reasons"); that's reasonable if you're giving a lecture where you have the opportunity to introduce new concepts in your preferred order and at your pace, but may not be practical in the random context of someone asking "hey, what is this (type a b . ...) code doing?". In practice I expect most non-expert users to consider it as a new, rather than derived, concept. 2. The syntax still suggests a semantic that is different from the actual one (ie. that the variables are bound locally to the type annotation), which could confuse users that don't even ask about it but simply assume it works somehow as they expect. I understand there are compromises at play here and am not too dissatisfied with this syntax, but still if it could be made unecessary by making the (type a) one scale to polymorphic recursion, I think that would be even better. > 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? In my opinion, errors should be for semantic errors, and warnings for "things that look like mistakes but are actually meaningful". In particular, errors are part of the language specification, while warnings are not. Making this cosmetic choice of "discouraging shadowing" an error makes it part of the semantic of the construct, while leaving it as a warning give it equivalent visibility, but with less urge to make sure that everyone really understands the situation. I also believe making part of the language semantics makes it even more difficult to get a clear and exhaustive mental model of the status of type variables: we already have 'a, '_a and a, maybe we don't also need non-uniform rules about when name conflicts and when they don't. (However, there is the argument that making this an error now leaves the option open to degrade it into a warning, while the reverse direction would break compatibility. I can understand the benefit keeping it that way for a coming release, even if those decisions usually have the unfortunate effect of keeping those warts with us much longer than originally hoped.) > 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. Indeed, instance values syntax is horrible -- I would be very frustrated if they were actually used. That's certainly not a good argument to introduce similar things, but I think you're pessimistic and the present situation is not as bad -- or maybe I haven't understood it in its full glory yet. > This is certainly doable, but in my opinion it would not replace the > "type a b. ..." syntax, which is more readable. Frankly, I don't think the extremely meager readability benefits outweigh the need to explain yet another kind of type annotation to the code readers. Compare: let rec length : type a b. (a,b) l -> 'a = function let rec length (type a b) : (a,b) l -> 'a = function And that's in the defavorable case of "function" which is friendly to function types annotations. In other situations you could replace the relatively awkward : a b . foo -> bar -> baz = fun x y -> .... by something like (type a b) (x : foo) (y : bar) : baz = ... in the cases where it is more readable -- you don't need to emphasize the whole function type. (Assuming, always, that the type-checker can detect the polymorphism for polymorphic recursion.) On Fri, Mar 23, 2012 at 7:45 AM, Jacques Garrigue wrote: > 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