[Caml-list] Re: Variance of GADT parameters

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

On 2012/02/13, at 2:36, Gabriel Scherer wrote:

> Thank you, Jacques and Jeremy, for the examples. Indeed that looks quite subtle.
> 
> I found it helpful to write an informal proof of covariance of the
> following type:
> 
>  type +_ expr =
>    | Val : 'a -> 'a expr
>    | Prod : 'a expr * 'b expr -> ('a * 'b) expr
> 
> Or, in a more explicit formulation using imaginary syntax with
> explicit existential variables and equalities.
> 
>  type +'a expr =
>    | Val of 'b . 'b with ('a = 'b)
>    | Prod of 'b 'c. 'b expr * 'c expr with ('a = 'b * 'c)
> 
> The informal proof goes as follow: assuming α ≤ α', we wish to show
> that α expr ≤ β expr. For a given (t : α expr):
>  - if (t) is (Val (v : α)), then by α ≤ α' we have (v : α') so (Val v
> : α' expr)
>  - if (t) is Prod((t1 : β expr), (t2 : γ expr)), with (α = β * γ), then
>    we have (β * γ ≤ α'). *By inversion* we know that there must exist
> β', γ' with
>    α' = β' * γ', β ≤ β' and γ ≤ γ'. We therefore have (t1 : β' expr),
> (t2 : γ' expr),
>    and therefore (Prod(t1,t2) : α' expr)
> 
> The core of the proof is an inversion lemma for subtyping at product types:
>    if β*γ ≤ α' then α' is of the form β'*γ' with β≤β', γ≤γ'
> 
> The strength of the inversion lemma depends a lot on the details of
> the theory. For example, if α = int and α ≤ α', do we have α' = int?
> And if α ≥ α'? I believe the answer to the α ≤ α' case is "yes", which
> would make the (type +_ expr = Const : int -> int expr) case correctly
> covariant, but as Jacques showed the answer is no in the contravariant
>  case α ≥ α', we have (int ≥≠ private int).

[...]

> I'm going to think a bit more about this. What do you think of the
> "proof" in the Prod case? Is there such an inversion principle for the
> OCaml type theory?

The proof looks fine.
Subtyping in OCaml has not been much studied.
You can find a short draft attempting to specify the current behavior
on my publication page.
Again I wonder whether you are not going to get problems with abstraction.
At first sight, no: if when you define a GADT t, the type u is abstract, then
it will have no supertype in any environment where we use t.
But if you think more carefully, you realize that if in the future we allow
(gadt-)unification between abstract types, everything breaks, since abstract
types may end up having supertypes in a local environment.
So it looks like the only types you can allow for instantiation are concrete
datatypes and well-known types (abstract types defined in the initial environment
or in the current module).

Jacques Garrigue