From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <rathereasy@gmail.com>
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by yquem.inria.fr (Postfix) with ESMTP id 10B2CBC57
	for <caml-list@yquem.inria.fr>; Sat,  4 Dec 2010 22:06:57 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AqYAAEM8+kxKfVK0k2dsb2JhbACjJggVAQEBAQkJCgkRBB6lOIlpghmEAi6IVgEBAwWFRASEX4YPhgU
X-IronPort-AV: E=Sophos;i="4.59,299,1288566000"; 
   d="scan'208";a="91298468"
Received: from mail-wy0-f180.google.com ([74.125.82.180])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 04 Dec 2010 22:06:56 +0100
Received: by wyb29 with SMTP id 29so5936176wyb.39
        for <caml-list@yquem.inria.fr>; Sat, 04 Dec 2010 13:06:56 -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=19MwVMr/5JdrlqhRNP5ag1ts2072mzAL4QvYe9aWKVE=;
        b=kNvlSmaQuPv11uLzrYhpDO9xT1sIWilO5Xj/QPlYuCubTBJaD+rXDs/Von4INPlQiL
         2dtv9omc8v9trJUuUV33mzJGn3+nDDicdXkApZ+XHPXAR2Gi7RKBN7yOju0DMJCdDCeh
         kPPYdDXLz6gZxPqrc0K/yM/gFHQYF5Cit04SE=
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=JNCwBWAwbmp93RJU/dR5QU/GosnNvWHr9dyzBZVdcFHegRF3sRH5aSyMozyHlrq11L
         k8P1FrbF9pHFdy8XZOJjZSMa6tSMs1n1HObni4z25QXK5gUwJEEPxriGpku6GLei/79J
         XQmFjlaOFT1r6d40/5xZyM9gupzeNztViIQfo=
MIME-Version: 1.0
Received: by 10.227.141.137 with SMTP id m9mr3649071wbu.115.1291496816559;
 Sat, 04 Dec 2010 13:06:56 -0800 (PST)
Received: by 10.227.11.71 with HTTP; Sat, 4 Dec 2010 13:06:56 -0800 (PST)
In-Reply-To: <AANLkTimRki9EfbN0ekQQA2RmaQ2u28pHuvy37-eLhtxq@mail.gmail.com>
References: <AANLkTimVTv7J_b6AY1gKKT9hdQx83a+4FBM7pqvHpAHM@mail.gmail.com>
	<AANLkTimmAMG_1+UhNh+Q8bR22XsDtoF44gDd7YEwx5v+@mail.gmail.com>
	<AANLkTim5uyeAXwSzvsVtDyQi28kqdKfE2hDOeCnRW+4Z@mail.gmail.com>
	<AANLkTi=brs65VkfeM0qt+fLFVd=Vc7PMm809VstVN=Q-@mail.gmail.com>
	<AANLkTin9Bdea8CZjx3OR1NsFFawSu7G8KGD_ZiTvGr1S@mail.gmail.com>
	<AANLkTimRki9EfbN0ekQQA2RmaQ2u28pHuvy37-eLhtxq@mail.gmail.com>
Date: Sat, 4 Dec 2010 16:06:56 -0500
Message-ID: <AANLkTi=tXmna=Rk5nyQbYWNambBYUUk1=nRS=aGC0cfV@mail.gmail.com>
Subject: Re: [Caml-list] GADT constructor syntax
From: Jacques Le Normand <rathereasy@gmail.com>
To: Lukasz Stafiniak <lukstafi@gmail.com>
Cc: caml-list caml-list <caml-list@yquem.inria.fr>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Spam: no; 0.00; syntax:01 lukasz:01 constructors:01 constructors:01 unifying:01 wrote:01 wrote:01 typing:01 caml-list:01 constructor:01 constructor:01 constraint:01 constraint:01 int:01 int:01 

in this case, yes, but if you have constraints then it is different. consid=
er:

type 'a term =3D
      | Ignore of 'a : int term
      | Embed of 'a
   constraint 'a =3D int

this is different from:

type 'a term =3D
     | Ignore of 'a : int term
     | Embed of 'a : 'a term
   constraint 'a =3D int

(in fact, an error is flagged on the second one)

Also, it can save the user some typing.

On Sat, Dec 4, 2010 at 4:00 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote=
:
> On Sat, Dec 4, 2010 at 9:54 PM, Jacques Le Normand <rathereasy@gmail.com>=
 wrote:
>> you may want to name your type parameters because you can mix GADT
>> constructors with normal constructors. consider:
>>
>> type 'a term =3D
>> =A0 =A0 | Ignore of 'a term : int term
>> =A0 =A0 | Embed of 'a
>>
>> I don't think propagating type parameters is a good idea. The current
>> rule is: ignore type parameters in GADT constructors. This is simpler
>> than unifying the type parameters with the arguments of the return
>> type of the constructor.
>
> But it expands to:
>
>> type 'a term =3D
>> =A0 =A0 | Ignore of 'a term : int term
>> =A0 =A0 | Embed of 'a : 'a term
>