Re: [Caml-list] GADT constructor syntax

[Lukasz Stafiniak <lukstafi@gmail.com>]

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

> 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.