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 73886BC58 for ; Mon, 25 Oct 2010 11:45:11 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAD7uxEzRVdi0kGdsb2JhbACTOIYbAYc2SwgVAQEBAQkJDAcRAx+gFolYgheFYC6IVwEBAwWFQwSBWohzhW+DKQ X-IronPort-AV: E=Sophos;i="4.58,235,1286143200"; d="scan'208";a="75729358" Received: from mail-qy0-f180.google.com ([209.85.216.180]) by mail4-smtp-sop.national.inria.fr with ESMTP; 25 Oct 2010 11:45:10 +0200 Received: by qyk8 with SMTP id 8so1328411qyk.18 for ; Mon, 25 Oct 2010 02:45:09 -0700 (PDT) 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=ddUI82w4mIC9d2hwohoIT6LOVkejZo01BliVTOPLUqQ=; b=b1B2ApABsDSfSO6m50150Y8Rbn8JkMu0radbx8YoPxg2HI8ICRW1a+VcaRN8xBHcPi iHSTrx52K775scO8S25rH8LmQmKJnsaQ5fyqy8tOJopGAkJYP5gPfnCDczUBV8tMUzBs 45seqXo4sQQpJ9Zm54j/OzBgbTrP4P2ka5Oms= 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=CVcOI7r/ZXRlHtgXEsYSSBU7q6yR6nl52sADztT7CBXLxiD2IBTwL3Dm6dOPCSavT7 FUNeEE8Q693urB1g6BI7RoqQrbP+AJbLBpWh6MgolS8EPOmfL6Y90XS0p+dyuYGcej/k 5uQbrqsAyJMTwIVF2GWClguOdMrUmuZW/JAzE= Received: by 10.229.81.15 with SMTP id v15mr748226qck.115.1287999909706; Mon, 25 Oct 2010 02:45:09 -0700 (PDT) MIME-Version: 1.0 Sender: gabriel.scherer@gmail.com Received: by 10.229.28.210 with HTTP; Mon, 25 Oct 2010 02:44:48 -0700 (PDT) In-Reply-To: References: From: bluestorm Date: Mon, 25 Oct 2010 11:44:48 +0200 X-Google-Sender-Auth: aWLqVv33T1-Srf8AeryrCX_sfIM Message-ID: Subject: Re: [Caml-list] Generalized Algebraic Datatypes To: Jacques Le Normand Cc: caml-list caml-list Content-Type: multipart/alternative; boundary=00163646d6a416bc1304936dd912 X-Spam: no; 0.00; datatypes:01 unifications:01 checker:01 checker:01 bool:01 subtype:01 bool:01 variants:01 syntax:01 trolls:01 foo:01 syntax:01 polymorphism:01 o'caml:01 compiler:01 --00163646d6a416bc1304936dd912 Content-Type: text/plain; charset=ISO-8859-1 It's very interesting. First, I'm curious of the "historical" aspects of this work : where does it come from ? Apparently there is work from you and Jacques Garrigue, but it's hard to tell. Is it new, or a long-running experiment ? In your "intuition" section (btw. there is a typo here, it should be (type s) (x : s t)), you seem to present GADT as directly related to the new (type s) construct. It's a bit surprising because it's difficult to know the difference between this and classic type variables. I suppose it is because only (type s) guarantee that the variable remains polymorphic, and you use that to ensure that branch-local unifications don't "escape" to the outer level ? Could you be a bit more explicit on this ? It's also a bit difficult to know what's the big deal about "exhaustiveness checks". As I understand it, you remark that with GADTs some case cannot happen due to typing reasons, but the exhaustive check doesn't know about it. Could you be a bit more explicit about what the exhaustiveness checker does : - is it exactly the same behavior as before, ignoring GADT specificities ? (ie. you haven't changed anything) - if not, what have you changed and how can we try to predict its reaction to a given code ? - what can we do when it doesn't detect an impossible case ? I suppose we can't a pattern clause for it, as the type checker would reject it. I'm not sure I understand the example of the "Variance" section. Why is the cast in that direction ? It seems to me that even if we could force t to be covariant, this cast (to a less general type) shouldn't work : # type +'a t = T of 'a;; # let a = T (object method a = 1 end);; # (a :> < m : int; n : bool > t);; Error: Type < a : int > t is not a subtype of < m : int; n : bool > t Again, you "Objects and variants" and "Propagation" subsections are a bit vague. Could you give example of code exhibiting possible problems ? Finally, a few syntax trolls, in decreasing order of constructivity : - is it a good idea to reproduce the "implicit quantification" of ordinary types ? It seems it could be particularly dangerous here. for example, changing type _ t = Id : 'a -> 'a t to type 'a t = Id : 'a -> 'a t | Foo of 'a introduce, if I'm not mistaken, a semantic-changing variable captures. (I thought other dark corners of the type declarations already had this behavior, but right now I can't remember which ones) - if I understand it correctly, (type a . a t -> a) is yet another syntax for type quantification. Why ? I thought (type a) was used to force generalization, but ('a . ...)-style annotation already force polymorphism (or don't they ?). Is it a semantic difference with ('a . 'a t -> 'a), other than its interaction with gadts ? Can we use (type a . a t -> a) in all places where we used ('a . 'a t -> 'a) before ? - is there a rationale for choosing Coq-style variant syntax instead of just adding a blurb to the existing syntax, such as | IntLit of int : int t or | IntList of int return int t ? Thanks. On Mon, Oct 25, 2010 at 10:39 AM, Jacques Le Normand wrote: > Dear Caml list, > > I am pleased to announce an experimental branch of the O'Caml compiler: > O'Caml extended with Generalized Algebraic Datatypes. You can find more > information on this webpage: > > https://sites.google.com/site/ocamlgadt/ > > > And you can grab the latest release here: > > svn checkout https://yquem.inria.fr/caml/svn/ocaml/branches/gadts > > > > Any feedback would be very much appreciated. > > Sincerely, > > Jacques Le Normand > > > _______________________________________________ > 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 > > --00163646d6a416bc1304936dd912 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
It's very interesting.

First, I'm curi= ous of the "historical" aspects of this work : where does it come= from ? Apparently there is work from you and Jacques Garrigue, but it'= s hard to tell. Is it new, or a long-running experiment ?

In your "intuition" section (btw. there is a typo = here, it should be (type s) (x : s t)), you seem to present GADT as directl= y related to the new (type s) construct. It's a bit surprising because = it's difficult to know the difference between this and classic type var= iables. I suppose it is because only (type s) guarantee that the variable r= emains polymorphic, and you use that to ensure that branch-local unificatio= ns don't "escape" to the outer level ? Could you be a bit mor= e explicit on this ?

It's also a bit difficult to know what's the bi= g deal about "exhaustiveness checks". As I understand it, you rem= ark that with GADTs some case cannot happen due to typing reasons, but the = exhaustive check doesn't know about it. Could you be a bit more explici= t about what the exhaustiveness checker does :
- is it exactly the same behavior as before, ignoring GADT specificiti= es ? (ie. you haven't changed anything)
- if not, what have y= ou changed and how can we try to predict its reaction to a given code ?
- what can we do when it doesn't detect an impossible case ? I sup= pose we can't a pattern clause for it, as the type checker would reject= it.

I'm not sure I understand the example of = the "Variance" section.
Why is the cast in that direction ? It seems to me that even if we cou= ld force t to be covariant, this cast (to a less general type) shouldn'= t work :

=A0=A0# type +'a t =3D T of 'a;;<= /div>
=A0=A0# let a =3D T (object method a =3D 1 end);;
=A0= =A0# (a :> < m : int; n : bool > t);;
=A0=A0Error: Type = < a : int > t is not a subtype of < m : int; n : bool > t=A0

Again, you "Objects and variants" and "Propagatio= n" subsections are a bit vague. Could you give example of code exhibit= ing possible problems ?

Finally, a few syntax trol= ls, in decreasing order of constructivity :

- is it a good idea to reproduce the "implicit qua= ntification" of ordinary types ? It seems it could be particularly dan= gerous here.
=A0=A0for example, changing
=A0=A0 =A0type= _ t =3D Id : 'a -> 'a t
=A0=A0to=A0
=A0=A0 =A0type 'a t =3D Id : 'a -> &#= 39;a t | Foo of 'a
=A0=A0introduce, if I'm not mistaken, = a semantic-changing variable captures.
=A0=A0(I thought other dar= k corners of the type declarations already had this behavior, but right now= I can't remember which ones)

- if I understand it correctly, (type a . a t -> a) = is yet another syntax for type quantification. Why ? I thought (type a) was= used to force generalization, but ('a . ...)-style annotation already = force polymorphism (or don't they ?). Is it a semantic difference with = ('a . 'a t -> 'a), other than its interaction with gadts ? C= an we use (type a . a t -> a) in all places where we used ('a . '= ;a t -> 'a) before ?

- is there a rationale for choosing Coq-style variant s= yntax instead of just adding a blurb to the existing syntax, such as
<= div>=A0=A0 =A0| IntLit of int : int t
=A0=A0or
=A0=A0 = =A0| IntList of int return int t
=A0=A0?


Thanks.

=
On Mon, Oct 25, 2010 at 10:39 AM, Jac= ques Le Normand=A0<rathereasy@gmail.com>=A0wrote:
Dear Caml list,

I am pleased to announce an experimental= branch of the O'Caml compiler: O'Caml extended with Generalized Al= gebraic Datatypes. You can find more information on this webpage:


=

And you can grab the latest release here:

svn checkout https://yquem.inria.fr/caml/svn/ocaml/branches/gadts 



Any feedback would be very much appreciated.

Since=
rely,

Jacques Le Normand


_______________________________________________ Caml-list mailing list. Subscription management:
http://yque= m.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives:=A0http://caml.inria.fr
Beginner's list:=A0http://groups.yahoo.com/group/ocaml_beginnersBug reports:=A0http://caml.inria.fr/bin/caml-bugs

--00163646d6a416bc1304936dd912--