Re: [Caml-list] GADT constructor syntax

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2010/12/05, at 17:35, bluestorm wrote:

> I'm not sure I see the point of this long discussion between Lukasz and Jacques.
> 
> It seems everybody agree that it is a good idea to explicitely quantify the constructor-specific type variables.
> 
> The question Jacques raised is wether, when we write (| Foo of 'a . S : T) or (| Foo : 'a . S -> T), the 'a is quantified on S only, or on both S and T. 
> 
> It think we all agree that, for semantical reasons, quantification should be scoped over both S and T. However, the (of S : T) syntax does not make it very obvious, and this should be rightfully considered as a defect of this syntax.
> 
> I'm under the impression that your intense debate is about the edge case where :
> 1. we don't use explicit quantification of constructor-specific variables
> 2. we reuse the type parameter variables in the type of a GADT constructor (so they're implicitly shadowed by the implicit quantifications, or maybe not)
> 
> If we reject possibly 1. (and ask for explicit quantification), all is well. If you want to consider option 1., then I think the edge case 2. is evil and shoud result in a warning.

Actually I'm not sure that fully explicit quantification is necessary, or even desirable.
The reason is that the gadt extension introduces actually two kinds of case-specific
type variables: universals and existentials.

Namely, in the type

  type _ term =
      Int : int -> int term
    | Bool : bool -> bool term
    | Lam : ('a -> 'b) -> ('a -> 'b) term
    | App : ('a -> 'b) * 'a -> 'b term

the type variables 'a and 'b in Lam are universals, but
in App only 'b is universal, while 'a is existential.

Personally, I would prefer this to be written:

  type _ term =
      Int of int : int term
    | Bool of bool : bool term
    | Lam of ('a -> 'b) : ('a -> 'b) term
    | App of 'a. ('a -> 'b) * 'a : 'b term

That is, use a syntax close to the current ocaml one, which makes
easy to quantify clearly existential variables, so that they cannot
be confused with universal ones. If we use the arrow syntax,
the natural scope for quantification includes the return type, which
is incorrect for existential types. And using the "of" syntax, it is hard
to quantify type variables appearing in the return type, so I think
this is better to leave the universals implicit.

Considering the definition

  type 'a t = Foo of 'a : 'b t

I think that is should either unify 'a and 'b, being in practice
equivalent to "type 'a t = Foo of 'a", or flag an error because 'a is not
available in this branch. I might actually prefer the unification approach,
because this conforms to the intuition that the scope of 'a is the whole
type definition, but maybe people can come to understand that an
explicit return type overrides this.

Jacques Garrigue