From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 38010BC57 for ; Sat, 4 Dec 2010 20:42:02 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArgAAJMo+kzRVdg0kGdsb2JhbACQX5JHCBUBAQEBCQkMBxEEHqVUiWmCGYQULohWAQEDBYVEBIpuhgU X-IronPort-AV: E=Sophos;i="4.59,299,1288566000"; d="scan'208";a="81721002" Received: from mail-qw0-f52.google.com ([209.85.216.52]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Dec 2010 20:41:37 +0100 Received: by qwe4 with SMTP id 4so5147560qwe.39 for ; Sat, 04 Dec 2010 11:41:36 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:mime-version:received:in-reply-to :references:from:date:message-id:subject:to:cc:content-type :content-transfer-encoding; bh=T41SPF8/ZNPpDvCdlJnv2jNA+TlARn8+PoRaIhNTT7M=; b=ZKZhmrNdfB/h54RUFgM4DLNPVFo1K3rHJfKF1nLI9eSIyIk7FdPL4E73uoJf7Ar6Fc vCJltbfiLWg8+4ohAXH3eAb18EJeVs+eeCXVrGxzb0iV9wzcebDQxb/BhIsd+TEciTj/ 3KpKBfnA/k7I2IoAzzKXeJiwkf7vI9wYluIUA= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=g4yQr5kFdD86N7ClOx/VpUtai35L9hI5bFt0Tms3TTLwP9+dERPUwNho8dvHR1NYRL KA/rL+TGs2JkyWeEr7t2dvOPn7wjGj+S2EqP6rjXTby6U9bAHdVeC3qHUXcdbmyh5oVo LUmQEnq81kgMpbX2mtygcFHJmHzrjisDp/iKg= Received: by 10.229.189.4 with SMTP id dc4mr2609502qcb.106.1291491696075; Sat, 04 Dec 2010 11:41:36 -0800 (PST) MIME-Version: 1.0 Received: by 10.229.230.149 with HTTP; Sat, 4 Dec 2010 11:41:15 -0800 (PST) In-Reply-To: References: From: Lukasz Stafiniak Date: Sat, 4 Dec 2010 20:41:15 +0100 Message-ID: Subject: Re: [Caml-list] GADT constructor syntax To: Jacques Le Normand Cc: caml-list caml-list Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; lukasz:01 syntax: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 Hi! Just a quick answer for now. On Sat, Dec 4, 2010 at 8:25 PM, Jacques Le Normand w= rote: > 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 > 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.