From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <rathereasy@gmail.com>
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
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 D069FBC57
	for <caml-list@yquem.inria.fr>; Sat,  4 Dec 2010 20:25:02 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AqcAAB4k+kxKfVK0k2dsb2JhbACQX5JHCBUBAQEBCQkKCREEHqVXiWmCGYQYLohWAQEDBYVEBIRfhg8
X-IronPort-AV: E=Sophos;i="4.59,299,1288566000"; 
   d="scan'208";a="69590990"
Received: from mail-wy0-f180.google.com ([74.125.82.180])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Dec 2010 20:25:02 +0100
Received: by wyb29 with SMTP id 29so5883978wyb.39
        for <caml-list@yquem.inria.fr>; Sat, 04 Dec 2010 11:25:01 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=domainkey-signature:mime-version:received:received:date:message-id
         :subject:from:to:content-type;
        bh=+85/S+yp8MvYbaVjol4FP08lNs5qHvMht0X35auIKXI=;
        b=B8eiRMpcOwyX5BNGNHGzA42mwTmTwmtSwwdLJsAiK2Wiwx96ld/pV3rItcbatr7n0r
         Z7RyOd9Kg+lSJJ2Yj8O1CEg8xdvx6ukziiZWj/iGBUVL7nVYfzn9NLK2jslaG8HGK7Ib
         p5BHZLaPUSGCx6r8k1MkglYRzUmJ65u5xuvZ0=
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=gamma;
        h=mime-version:date:message-id:subject:from:to:content-type;
        b=DL5jheD5o4H9ja3Vgxm2GR1EsD+fFRZ6OTq1ncCAlHMGvgnafGgIsLm6hwPOTRfk8q
         x9Im87wZTTT5LbTYFUn/U5qs4knh6jni+SjS2Vyij4GiMu+8JYFDAA6nA13NYiqnHIF5
         eadqeSUeCYSLu6ETvbqZqPAsPMo9TVmZ+ktK4=
MIME-Version: 1.0
Received: by 10.227.68.206 with SMTP id w14mr3559981wbi.144.1291490701631;
 Sat, 04 Dec 2010 11:25:01 -0800 (PST)
Received: by 10.227.11.71 with HTTP; Sat, 4 Dec 2010 11:25:01 -0800 (PST)
Date: Sat, 4 Dec 2010 14:25:01 -0500
Message-ID: <AANLkTimVTv7J_b6AY1gKKT9hdQx83a+4FBM7pqvHpAHM@mail.gmail.com>
Subject: GADT constructor syntax
From: Jacques Le Normand <rathereasy@gmail.com>
To: caml-list caml-list <caml-list@yquem.inria.fr>
Content-Type: text/plain; charset=ISO-8859-1
X-Spam: no; 0.00; syntax:01 syntax:01 constructors:01 ocaml:01 bool:01 bool:01 constructors:01 foo:01 intuitively:01 foo:01 forall:01 existential:01 existential:01 quantified:01 quantified:01 

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 =
        TrueLit : bool t
      | IntLit of int : int lit

option b)

type _ t =
      TrueLit : bool t
    | 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

Personal opinion:

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 = Foo of 'a : 'b t

this, counter intuitively, creates a constructor Foo of type forall 'd
'e. 'd t -> 'e t.

2) explicit quantification of existential variables

option a)

leave existential variables implicitly quantified. For example:

type _ u = Bar of 'a t : u
or
type _ u = Bar :  'a t -> u

option b)

specifically quantify existential variables. For example:

type _ u = Bar of 'a. 'a t : u
or
type _ u = Bar : 'a. 'a t -> u

Currently, the branch uses option a).

Personal opinion: I prefer option b). This is for four reasons:

I) the scope of the explicitly quantified variable is not clear. For
example, how do you interpret:

type _ u = Bar of 'a. 'a : 'a t
or
type _ u = 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. My
inclination would be to flag it as an error.

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.

III) option a) is the current Haskell GADT syntax and I've never heard
anyone complain about it

IIII) I don't see how option b) improves either readability or bug prevention

I look forward to hearing your opinions.

--Jacques Le Normand