Re: [Caml-list] GADT constructor syntax

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

see below

On Sat, Dec 4, 2010 at 2:41 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> Hi! Just a quick answer for now.
>
> On Sat, Dec 4, 2010 at 8:25 PM, Jacques Le Normand <rathereasy@gmail.com> 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 =
>>        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
>
> 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 = 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 = 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 = 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).
>
> 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 = 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.
>
> 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.
>