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 q2N5r6wR010294 for ; Fri, 23 Mar 2012 06:53:12 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ai0CADgPbE/RVdc2kGdsb2JhbABEDqYNkTgIIgEBAQEJCQ0HFAQjggkBAQEDARICExkBGxILAQMBCwYFCw0NISIBEQEFAQoSBhMICgkHh2MFC5ozCowWgnGFBD+IdgEFC5B4BJVfjkk9g1I4 X-IronPort-AV: E=Sophos;i="4.73,634,1325458800"; d="scan'208";a="150828167" Received: from mail-lpp01m010-f54.google.com ([209.85.215.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 Mar 2012 06:53:00 +0100 Received: by lagv3 with SMTP id v3so3876624lag.27 for ; Thu, 22 Mar 2012 22:53:00 -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=y9EZgoDNcApbtXQH/h7BbbbFv5T/eEdU4fbL7A9bUyI=; b=pb0+1dCYPM7SkhidlxUrf+Ns2iMdlohhM3eeRKTcUBxIEUGPatZHvqCFuGaN8APNBf doDk2Tf8gf7lTdDPrO5qsL3cLT/Dt1D+diR6uS5YFKFw7l0rUcoKj83CiPPXsPNkbpLq t3UmsmgeK2RWd2kKlsOY1eKjmXs8TZBH9Rb2Ipcs6MQU8uroKW/3ImHNlnhwmAYWNFjI oNTSfImCP3k+SLL80JBn75iQ5EpgX4GW4Skf4JMiJxk7Lh3Ipbu9wtdOoEHeQSxcKEVQ tpsBbfFagNDN67L6bT4qyhW9PniRKgUFBzE3KXhTGVZW5MlebE/BiRG/6YRb77JjZS2f M2VA== Received: by 10.112.85.136 with SMTP id h8mr3941849lbz.72.1332481978568; Thu, 22 Mar 2012 22:52:58 -0700 (PDT) MIME-Version: 1.0 Received: by 10.112.130.233 with HTTP; Thu, 22 Mar 2012 22:52:18 -0700 (PDT) In-Reply-To: References: <20120322095143.GA30016@voyager> From: Gabriel Scherer Date: Fri, 23 Mar 2012 06:52:18 +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 q2N5r6wR010294 Subject: Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS? > 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. > 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. 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. (On my wishlist: ... (type a) (type b) ... could be written ... (type a b) ...) On Thu, Mar 22, 2012 at 11:12 PM, Jacques Garrigue wrote: > 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 > > -- > Caml-list mailing list.  Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >