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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 7435EBBAF for ; Fri, 29 Oct 2010 17:54:05 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhoBAHSLykxKfVK0kGdsb2JhbACTKo4iCBUBAQEBCQkMBxEDH6QSiVmCF4YaLohXAQEDBYVDBIpThXQ X-IronPort-AV: E=Sophos;i="4.58,260,1286143200"; d="scan'208";a="77394832" Received: from mail-wy0-f180.google.com ([74.125.82.180]) by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Oct 2010 17:53:49 +0200 Received: by wyb32 with SMTP id 32so3178875wyb.39 for ; Fri, 29 Oct 2010 08:53:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:in-reply-to :references:date:message-id:subject:from:to:cc:content-type; bh=/1NFJ+XNik0X/gXVBFmlk60+pgQg+e/TOyooSEcjZNg=; b=sryn3GmAC9ZAw2+4COQDUxf39jGidvFMlxVfL8Em5SjdQDybcZvzNNl7rl/CJON6E6 zjrWyqna+uL487U5zNE443iG86wtTx/cO9j6Bo5Of6PafsIqUsiXGa5OlkXlTDgKokTR EJeXJbWYZP3Yx2Oo339dIlWa3+bruf5McTx7s= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=HN1ykKYHDHfsgFRa0MUFZPa+w7emkDpnN9A5wfk8horvx8Gmt1KwK60aw6X8JLWhid ChAgDqOqpJD0ByR1m2NqxK6M2ubYuNa+GSExC6P4zFz/IFhnrWIPxNFZivyyBe5L12gW fBv61S2WowktZVyh4wNR1fRQX7aQIG6qdJzX4= MIME-Version: 1.0 Received: by 10.227.136.194 with SMTP id s2mr7890894wbt.6.1288367628699; Fri, 29 Oct 2010 08:53:48 -0700 (PDT) Received: by 10.216.161.12 with HTTP; Fri, 29 Oct 2010 08:53:48 -0700 (PDT) In-Reply-To: <904846.44200.qm@web111513.mail.gq1.yahoo.com> References: <904846.44200.qm@web111513.mail.gq1.yahoo.com> Date: Fri, 29 Oct 2010 11:53:48 -0400 Message-ID: Subject: Re: [Caml-list] Generalized Algebraic Datatypes From: Jacques Le Normand To: Dario Teixeira Cc: caml-list Content-Type: multipart/alternative; boundary=0016e657b29ed949030493c3760a X-Spam: no; 0.00; datatypes:01 syntax:01 syntax:01 cheers:01 o'caml:01 compiler:01 o'caml:01 datatypes:01 bool:01 bool:01 constructors:01 haskell:01 ocaml:01 ocaml:01 verbose:01 --0016e657b29ed949030493c3760a Content-Type: text/plain; charset=ISO-8859-1 Assuming I understand this syntax, the following currently valid type definition would have two interpretations: type 'a t = IntLit of 'a constraint 'a = int One interpretation as a standard constrained ADT and one interpretation as a GADT. We could use another token, other than constraint, for example: type 'a t = IntLit of 'a : 'a = int to which I have no objections. As you pointed out, though, the current syntax is more concise. cheers, --Jacques On Fri, Oct 29, 2010 at 10:32 AM, Dario Teixeira wrote: > Hi, > > > 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: > > I have a couple of questions regarding the syntax you've chosen for GADT > declaration. For reference, let's consider the first example you've > provided: > > type _ t = > | IntLit : int -> int t > | BoolLit : bool -> bool t > | Pair : 'a t * 'b t -> ('a * 'b) t > | App : ('a -> 'b) t * 'a t -> 'b t > | Abs : ('a -> 'b) -> ('a -> 'b) t > > > There's something "Haskellish" about this syntax, in the sense that type > constructors are portrayed as being like functions. While this does make > sense in Haskell, in Ocaml it feels a bit out of place, because you cannot, > for example, partially apply a type constructor. > > Also, note that in all the variant declarations the final token is 't'. > Are there any circumstances at all where a GADT constructor will not end > by referencing the type being defined? If there are not, then this syntax > imposes some syntactic salt into the GADT declaration. > > I know this is not the sole syntax that was considered for GADTs in Ocaml. > Xavier Leroy's presentation in CUG 2008 shows a different one, which even > though slightly more verbose, does have the advantage of being more > "Camlish". > Is there any shortcoming to the 2008 syntax that resulted in it being > dropped > in favour of this new one? > > Best regards, > Dario Teixeira > > > > > --0016e657b29ed949030493c3760a Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Assuming I understand this syntax, the following currently valid type defin= ition would have two interpretations:

type 'a t = =3D IntLit of 'a constraint 'a =3D int

One= interpretation as a standard constrained ADT and one interpretation as a G= ADT. We could use another token, other than constraint, for example:

type 'a t =3D IntLit of 'a : 'a =3D int
=
to which I have no objections. As you pointed out, though, t= he current syntax is more concise.=A0

cheers,
--Jacques

On Fri, Oct 29, 2010 at 10:32= AM, Dario Teixeira <darioteixeira@yahoo.com> wrote:
Hi,

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

I have a couple of questions regarding the syntax you've chosen f= or GADT
declaration. =A0For reference, let's consider the first example you'= ;ve provided:

type _ t =3D
=A0| IntLit : int -> int t
=A0| BoolLit : bool -> bool t
=A0| Pair : 'a t * 'b t -> ('a * 'b) t
=A0| App : ('a -> 'b) t * 'a t -> 'b t
=A0| Abs : ('a -> 'b) -> ('a -> 'b) t


There's something "Haskellish" about this syntax, in the sens= e that type
constructors are portrayed as being like functions. =A0While this does make=
sense in Haskell, in Ocaml it feels a bit out of place, because you cannot,=
for example, partially apply a type constructor.

Also, note that in all the variant declarations the final token is 't&#= 39;.
Are there any circumstances at all where a GADT constructor will not end by referencing the type being defined? =A0If there are not, then this synta= x
imposes some syntactic salt into the GADT declaration.

I know this is not the sole syntax that was considered for GADTs in Ocaml.<= br> Xavier Leroy's presentation in CUG 2008 shows a different one, which ev= en
though slightly more verbose, does have the advantage of being more "C= amlish".
Is there any shortcoming to the 2008 syntax that resulted in it being dropp= ed
in favour of this new one?

Best regards,
Dario Teixeira





--0016e657b29ed949030493c3760a--