Re: [Caml-list] GADT constructor syntax

[Jacques Le Normand <rathereasy@gmail.com>]

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

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

this is different from:

type 'a term =
     | Ignore of 'a : int term
     | Embed of 'a : 'a term
   constraint 'a = 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 =
>>     | Ignore of 'a term : int term
>>     | 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 =
>>     | Ignore of 'a term : int term
>>     | Embed of 'a : 'a term
>