From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 6FA03BBAF for ; Mon, 6 Dec 2010 01:22:01 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoABAO+7+0zRVdW0gWdsb2JhbACYLop6CBUBAQsJChoEHqQ4jAKEBokEAQEDBYVEBIRdhhGDe4U4 X-IronPort-AV: E=Sophos;i="4.59,303,1288566000"; d="scan'208";a="82042367" Received: from mail-yx0-f180.google.com ([209.85.213.180]) by mail4-smtp-sop.national.inria.fr with ESMTP; 06 Dec 2010 01:21:44 +0100 Received: by yxm34 with SMTP id 34so2003443yxm.39 for ; Sun, 05 Dec 2010 16:21:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:sender:subject:mime-version :content-type:from:in-reply-to:date:cc:content-transfer-encoding :message-id:references:to:x-mailer; bh=Y2y+bor2kBqqIcCwkDSvOHnIZ57CFi2YamLmmrNXQfM=; b=M483jyoneSh3iBVRXnrTBma2Gx+SUjL260BkBu6YzmpA7VMmecWnCBjqlSKwKUG4f+ 6LXEnjw9CvAKIJhe1ho5uW9bKHOBG++OBFBTSqF57GB2Ge0i52o3cwWdMGeClLAnCu9P FJq3LcXmk/Hfw/hf/BAOAVtDzcnBr19TVkd1c= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=IQWecI/6mDcRKbniGRt0XAOV2at6f+1yfTDke0E02lNw0L1yuz0OKetyn03WkJVJxu n+A/HZ08VDZC5j0vciTqD0JhUOZKcgLi6O2oN5aX32t2BErjp+IE+VYOeCU75iNAMc0b mIxqJ9f8FBLtu5tkR7rRmJwEdsdGRfqu8m0J8= Received: by 10.150.196.2 with SMTP id t2mr8199223ybf.205.1291594903852; Sun, 05 Dec 2010 16:21:43 -0800 (PST) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id d4sm1306125ybi.0.2010.12.05.16.21.41 (version=TLSv1/SSLv3 cipher=RC4-MD5); Sun, 05 Dec 2010 16:21:43 -0800 (PST) Sender: Jacques Garrigue Subject: Re: [Caml-list] GADT constructor syntax Mime-Version: 1.0 (Apple Message framework v1082) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Mon, 6 Dec 2010 09:21:39 +0900 Cc: caml-list@yquem.inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: References: To: bluestorm X-Mailer: Apple Mail (2.1082) X-Spam: no; 0.00; syntax:01 lukasz:01 explicitely:01 foo:01 foo:01 quantified:01 syntax:01 bool:01 bool:01 existential:01 ocaml:01 existential:01 unify:01 unification:01 wrote:01 On 2010/12/05, at 17:35, bluestorm wrote: > I'm not sure I see the point of this long discussion between Lukasz = and Jacques. >=20 > It seems everybody agree that it is a good idea to explicitely = quantify the constructor-specific type variables. >=20 > The question Jacques raised is wether, when we write (| Foo of 'a . S = : T) or (| Foo : 'a . S -> T), the 'a is quantified on S only, or on = both S and T.=20 >=20 > It think we all agree that, for semantical reasons, quantification = should be scoped over both S and T. However, the (of S : T) syntax does = not make it very obvious, and this should be rightfully considered as a = defect of this syntax. >=20 > I'm under the impression that your intense debate is about the edge = case where : > 1. we don't use explicit quantification of constructor-specific = variables > 2. we reuse the type parameter variables in the type of a GADT = constructor (so they're implicitly shadowed by the implicit = quantifications, or maybe not) >=20 > If we reject possibly 1. (and ask for explicit quantification), all is = well. If you want to consider option 1., then I think the edge case 2. = is evil and shoud result in a warning. Actually I'm not sure that fully explicit quantification is necessary, = or even desirable. The reason is that the gadt extension introduces actually two kinds of = case-specific type variables: universals and existentials. Namely, in the type type _ term =3D Int : int -> int term | Bool : bool -> bool term | Lam : ('a -> 'b) -> ('a -> 'b) term | App : ('a -> 'b) * 'a -> 'b term the type variables 'a and 'b in Lam are universals, but in App only 'b is universal, while 'a is existential. Personally, I would prefer this to be written: type _ term =3D Int of int : int term | Bool of bool : bool term | Lam of ('a -> 'b) : ('a -> 'b) term | App of 'a. ('a -> 'b) * 'a : 'b term That is, use a syntax close to the current ocaml one, which makes easy to quantify clearly existential variables, so that they cannot be confused with universal ones. If we use the arrow syntax, the natural scope for quantification includes the return type, which is incorrect for existential types. And using the "of" syntax, it is = hard to quantify type variables appearing in the return type, so I think this is better to leave the universals implicit. Considering the definition type 'a t =3D Foo of 'a : 'b t I think that is should either unify 'a and 'b, being in practice equivalent to "type 'a t =3D Foo of 'a", or flag an error because 'a is = not available in this branch. I might actually prefer the unification = approach, because this conforms to the intuition that the scope of 'a is the whole type definition, but maybe people can come to understand that an explicit return type overrides this. Jacques Garrigue=