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 q2MNWkKJ025604 for ; Fri, 23 Mar 2012 00:32:46 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag0BAOK1a09KfVK2kGdsb2JhbABEDrcqCCIBAQEBCQkNBxQEI4IJAQEBBBICExMGARQkAQMMAQUFGC4UIAEFAQEhEwkSB4doBAeaUAqPB4UJiTUBBQsIilCFHmMElV6LM4MXPYFXgXs4gVs X-IronPort-AV: E=Sophos;i="4.73,633,1325458800"; d="scan'208";a="137343372" Received: from mail-we0-f182.google.com ([74.125.82.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 23 Mar 2012 00:32:41 +0100 Received: by wern13 with SMTP id n13so3825235wer.27 for ; Thu, 22 Mar 2012 16:32:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; bh=REjt5J+RpP+cfBjGKOKU/EoyyvTQl7B040l8FpKdEs0=; b=GcQhBLuV4j5ItIAObDh50JAK8lRnrvKM7xBvGz3HeSaZRhCMxmyp4zbXzrOkq00YcW /HMeJTzqDO0ht7b1nYzn2Bet82Xx0KmjWUF0XlVUBhc3ptJCwXbtTaTaEvLQZOrL+XSv Tl4NGSwxgQsUAO9H18aC7t9LJeJ2+NBc6LcJMmh2z8urfN6ssug5/rhvTIYub4r8J56/ wlKG7v/kN5cndQxEY5zP92uMKmCQNZ+8x0kEksLixD4GDYGQKswTFbbjSnbVpjy10sVK 7TsWQkMdz8n8I/Reu8z8qWbnI7IWStT2ajfaDJiK1hnn8LpbOjQ0e1bypceb3AEfwOaJ 2HgQ== Received: by 10.180.88.164 with SMTP id bh4mr896418wib.22.1332459160800; Thu, 22 Mar 2012 16:32:40 -0700 (PDT) Received: from voyager (bny92-3-81-56-44-163.fbx.proxad.net. [81.56.44.163]) by mx.google.com with ESMTPS id df3sm9145505wib.1.2012.03.22.16.32.39 (version=TLSv1/SSLv3 cipher=OTHER); Thu, 22 Mar 2012 16:32:39 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by voyager with local (Exim 4.72) (envelope-from ) id 1SArXw-0006DB-4H; Fri, 23 Mar 2012 00:35:56 +0100 Date: Fri, 23 Mar 2012 00:35:56 +0100 From: Roberto Di Cosmo To: Jacques Garrigue Cc: caml-list@inria.fr Message-ID: <20120322233556.GA23754@voyager> References: <20120322095143.GA30016@voyager> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.20 (2009-06-14) Subject: Re: [Caml-list] Funny name for a type variable in the output: should this be filed on the BTS? Dear Jacques, thanks for having looked into this issue and explaining its origin: if I understand well, this comes from a combination of two mechanisms (1) the desugaring of type a b. (a,b) l -> 'a into 'a1 'b. ('a1,'b) l -> 'a that introduces the 'a1 (2) the fact that the output type strives to respect the type variable names used in the user code : this brings the 'a1 over to the output type I think (2) is a useful feature: it may be hepful to see immediately where a type variable comes from. I would probably, as you did, point my finger at (1): the trouble seems to come from the fact that we can intermix unquoted type variables and quoted type variables in the same type. One may have very legitimate reasons to want an 'a in the type type a b. (a,b) l -> 'a but of course we do not expect a and 'a to be the same variable... --Roberto On Fri, Mar 23, 2012 at 07:12:52AM +0900, Jacques Garrigue wrote: > On 2012/03/22, at 18:51, Roberto Di Cosmo wrote: > > type empty > > type nonempty > > > > type ('a, 'b) l = > > Nil : (empty, 'b) l > > | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;; > > > > let rec length : type a b. (a,b) l -> 'a = function > > | Nil -> 0 > > | (Cons (_,r)) -> 1+ (length r);; > > > > look at the output type > > > > val length : ('a1, 'b) l -> int = > > > > 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 -- --Roberto Di Cosmo ------------------------------------------------------------------ Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo FRANCE. Twitter: http://twitter.com/rdicosmo ------------------------------------------------------------------ Attachments: MIME accepted, Word deprecated http://www.gnu.org/philosophy/no-word-attachments.html ------------------------------------------------------------------ Office location: Bureau 6C08 (6th floor) 175, rue du Chevaleret, XIII Metro Chevaleret, ligne 6 ------------------------------------------------------------------