From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id AB1CCBBAF for ; Sun, 5 Dec 2010 09:35:36 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtQAAEbd+kzRVdg0k2dsb2JhbACUa4YuAYc2WggVAQEBAQkJCgkRBB6kcYlpghmEBi6IVgEBAwWFRASBXIkShgWDLg X-IronPort-AV: E=Sophos;i="4.59,301,1288566000"; d="scan'208";a="69892435" Received: from mail-qw0-f52.google.com ([209.85.216.52]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Dec 2010 09:35:35 +0100 Received: by qwe4 with SMTP id 4so5392400qwe.39 for ; Sun, 05 Dec 2010 00:35:35 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:mime-version:sender:received :in-reply-to:references:from:date:x-google-sender-auth:message-id :subject:to:cc:content-type; bh=qwXL9a/kKBHbRb7dE//Y6vxlWPHUxZwAAh4aLPksZ0E=; b=SnA48nd1ekXYc26fHR7R9tufFB5nwBTyBUwaUzY0sWi+6dha5PvXX86vKPnQm4ebgY OJBv11IneRlolh7JeE6yAimVkestTEPgHlTijZdJCwC0VhXuMMXxzgIKUwlMqF9UOnvY kbVS/OAaGAg7cHMEeWdHG8DZ3dy9jfcoPOOzA= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=qfoLkMwHy/XqueKgbFFp5dG9Bq2EPse11D7gUP2CYFce96Z3cMA005NaSh2Rg92nJJ qnOsD8oBYBC/SEb+/TEmmmcaRuuYtck9JTUFZ9cRIQZsYzwlkFVQmw9FrxitJne22y0p zdESJtt08Tg4qhX1Q7KgO4jQ9uPwtfI7OXuGI= Received: by 10.229.230.197 with SMTP id jn5mr3057261qcb.274.1291538133140; Sun, 05 Dec 2010 00:35:33 -0800 (PST) MIME-Version: 1.0 Sender: gabriel.scherer@gmail.com Received: by 10.229.23.139 with HTTP; Sun, 5 Dec 2010 00:35:12 -0800 (PST) In-Reply-To: References: From: bluestorm Date: Sun, 5 Dec 2010 09:35:12 +0100 X-Google-Sender-Auth: wwzgUK4jkRJyd3rAeZafPdRGG-0 Message-ID: Subject: Re: [Caml-list] GADT constructor syntax To: Lukasz Stafiniak Cc: Jacques Le Normand , caml-list caml-list Content-Type: multipart/alternative; boundary=00163630ed43a3c57f0496a5a72a X-Spam: no; 0.00; syntax:01 lukasz:01 explicitely:01 foo:01 foo:01 quantified:01 syntax:01 lukasz:01 quantified:01 notation:01 existential:01 beginner's:01 ocaml:01 bug:01 explicitely:01 --00163630ed43a3c57f0496a5a72a Content-Type: text/plain; charset=ISO-8859-1 I'm not sure I see the point of this long discussion between Lukasz and Jacques. It seems everybody agree that it is a good idea to explicitely quantify the constructor-specific type variables. 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. 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. 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) 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. On Sun, Dec 5, 2010 at 9:25 AM, Lukasz Stafiniak wrote: > On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak > wrote: > > > > shouldn't mean that Embed is "basically" Embed of int : int term. My > > position is that if a type variable should be treated as local to a > > branch, it should be explicitly quantified (using the dot notation, > > for example "Ignore of 'a. 'a : int term", without any exceptions to > > "existential" variables). And that the patterns > > > > type X = > > | Branch of Y > > > > and > > > > type X = > > | Branch of Y : X > > > > should be equivalent (where X could for example be 'a term). > > To clarify again: modulo variable capture! That is, the pattern > > > type X = > > | Branch of 'a. Y : X > > will be different (unless 'a is not used in Y nor X). > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --00163630ed43a3c57f0496a5a72a Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable I'm not sure I see the point of this long discussion between Lukasz and= Jacques.

It seems everybody agree that it is a good ide= a to explicitely quantify the constructor-specific type variables.

The question Jacques raised is wether, when we write (|= Foo of 'a . S : T) or (| Foo : 'a . S -> T), the 'a is quan= tified on S only, or on both S and T.=A0

It think we all = agree that, for semantical reasons, quantification should be scoped over bo= th S and T. However, the (of S : T) syntax does not make it very obvious, a= nd this should be rightfully considered as a defect of this syntax.

I'm under the impression that your intense debate i= s about the edge case where :
1. we don't use explicit quanti= fication of constructor-specific variables
2. we reuse the type p= arameter variables in the type of a GADT constructor (so they're implic= itly shadowed by the implicit quantifications, or maybe not)

If we reject possibly 1. (and ask for explicit quantifi= cation), all is well. If you want to consider option 1., then I think the e= dge case 2. is evil and shoud result in a warning.


On Sun, Dec 5, 2010 at 9:25 = AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
>
> shouldn't mean that Embed is "basically" Embed of int : = int term. My
> position is that if a type variable should be treated as local to a > branch, it should be explicitly quantified (using the dot notation, > for example "Ignore of 'a. 'a : int term", without a= ny exceptions to
> "existential" variables). And that the patterns
>
> type X =3D
> =A0| Branch of Y
>
> and
>
> type X =3D
> =A0| Branch of Y : X
>
> should be equivalent (where X could for example be 'a term).

To clarify again: modulo variable capture! That is, the pattern

> type X =3D
> =A0| Branch of 'a. Y : X

will be different (unless 'a is not used in Y nor X).

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.in= ria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

--00163630ed43a3c57f0496a5a72a--