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 8F28CBC57 for ; Sat, 4 Dec 2010 21:14:52 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArgAANcv+kxKfVIukGdsb2JhbACQXpJHCBUBAQEBCQkMBxEEHqVGiWmCGYQOLohWAQEDBYVEBIRfhg+GBQ X-IronPort-AV: E=Sophos;i="4.59,299,1288566000"; d="scan'208";a="69608675" Received: from mail-ww0-f46.google.com ([74.125.82.46]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Dec 2010 21:14:52 +0100 Received: by wwj40 with SMTP id 40so4300647wwj.3 for ; Sat, 04 Dec 2010 12:14:51 -0800 (PST) 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 :content-transfer-encoding; bh=94g7D/rVvHSSnejxmDnlJRttX96BNpMgWTT31Df7xyw=; b=HLExpZfs5AN1gsRByWhvbf2FQEgLWXaI03SF6JYweQjaCCz0hl6+vKFBkS8KRfLDhL Atf8eRxN3HlOZ7O9w56WAJz8nasenw/Dga8E3OunMcrkNeHcwXqh/261vTWDGWWgSJM7 6QKQ7fcKEJA7m5L+zYqbbjYIXWDiRGkvsFXB0= 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:content-transfer-encoding; b=mKeaUJc8M1V3WAUZmM6h0axOa3aZSavd6eo/1CoD69ByZetZhES8gNTpgPOY9TBKIb Jej6m4v+vvdZWeN4U0WIJNJ73qgiNlBJYmr2MVAAPUU8I/+C45llGw5VfJT9VzssFHWy JcZG0G4b6VXCYEe/hvbcp2GlyHxk8nxPiYcbg= MIME-Version: 1.0 Received: by 10.227.147.196 with SMTP id m4mr3660208wbv.57.1291493691579; Sat, 04 Dec 2010 12:14:51 -0800 (PST) Received: by 10.227.11.71 with HTTP; Sat, 4 Dec 2010 12:14:51 -0800 (PST) In-Reply-To: References: Date: Sat, 4 Dec 2010 15:14:51 -0500 Message-ID: Subject: Re: [Caml-list] GADT constructor syntax From: Jacques Le Normand To: Lukasz Stafiniak Cc: caml-list caml-list Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; syntax:01 lukasz:01 syntax:01 constructors:01 ocaml:01 bool:01 bool:01 ocaml:01 notation:01 constructors:01 foo:01 intuitively:01 foo:01 forall:01 forall:01 see below On Sat, Dec 4, 2010 at 2:41 PM, Lukasz Stafiniak wrote= : > Hi! Just a quick answer for now. > > On Sat, Dec 4, 2010 at 8:25 PM, Jacques Le Normand = wrote: >> Dear caml-list, >> I would like to start a constructive discussion on the syntax of GADT >> constructors of the ocaml gadt branch, which can be found at: >> >> https://sites.google.com/site/ocamlgadt/ >> >> There are two separate issues: >> >> 1) general constructor form >> >> option a) >> >> type _ t =3D >> =A0 =A0 =A0 =A0TrueLit : bool t >> =A0 =A0 =A0| IntLit of int : int lit >> >> option b) >> >> type _ t =3D >> =A0 =A0 =A0TrueLit : bool t >> =A0 =A0| IntLit : int -> int lit >> >> I'm open to other options. The branch has used option b) from the >> start, but I've just switched to option a) to see what it's like > > I like option (a) for consistency with the existing OCaml syntax, and > while I like option (b) for its conformance to standard notation, I > don't like your reasons for liking (b) ;-) > > >> I slightly prefer option b), because it makes it clear that it's a >> gadt constructor right from the start. This is useful because the type >> variables in gadt constructors are independent of the type parameters >> of the type, consider: >> >> type 'a t =3D Foo of 'a : 'b t >> >> this, counter intuitively, creates a constructor Foo of type forall 'd >> 'e. 'd t -> 'e t. > > I think that the scope should propagate, i.e. that somehow the 'a > should really be bound, giving > > Foo : forall 'a . 'a t -> 'a t having type 'a t =3D Foo of 'a : 'b t creating a constructor of type forall 'a. 'a -> 'a t is really confusing since the user explicitly gave the return type of the constructor as 'b t. > >> 2) explicit quantification of existential variables > > I don't even like the problem formulation. I think that existential > variables should not be differentiated from universal variables. (So I > think I like what you don't like about the Haskell solution). >> >> option a) >> >> leave existential variables implicitly quantified. For example: >> >> type _ u =3D Bar of 'a t : u >> or >> type _ u =3D Bar : =A0'a t -> u >> >> option b) >> >> specifically quantify existential variables. For example: >> >> type _ u =3D Bar of 'a. 'a t : u >> or >> type _ u =3D Bar : 'a. 'a t -> u >> >> Currently, the branch uses option a). > > For me, it is a question for _all_ variables whether be implicitly or > explicitly quantified... > >> I) the scope of the explicitly quantified variable is not clear. For >> example, how do you interpret: >> >> type _ u =3D Bar of 'a. 'a : 'a t >> or >> type _ u =3D Bar : 'a. 'a -> 'a t >> >> In one interpretation bar has type forall 'a 'b. 'a -> 'b t and in >> another interpretation it has type forall 'a. 'a -> 'a t. > > Of course the "forall 'a. 'a -> 'a t" as far as I'm concerned! > >> II) >> >> In the example of option b), the 'a variable is quantified as a >> universal variable but, in patterns, it is used as an existential >> variable. This is something I found very confusing in Haskell where >> they actually use the 'forall' keyword. > > It often happens in logic! You have two sides of the turnstyle... > > I'm sorry if I sounded harsh, not my intention! > > Best Regards. >