[Caml-list] Re: Variance of GADT parameters

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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 β≤β', γ≤γ'

I believe this is true of OCaml product types, and can be generalized
to some other OCaml types. It would not be true if we had a top type,
and it would be unsafe to coerce (Prod (t1, t2)) into (⊤ expr) – this
is clear if we remove the Val case: if expr only had a Prod case, one
could write a function (⊤ expr → ⊥), with no case at all, that would
be accepted by the type-checker as ⊤ and ∃βγ.β*γ do not overlap.

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 think this technique of inversion can be generalized to arbitrary
GADT constructors
  type (α₁,α₂..αm) t =
    ...
  | C of ∃β₁β₂...βn. σ with (α₁ = τ₁, α₂ = τ₂... αm = τm)

I'm under the impression that they give something that looks a bit
like my previous conditions, with additional restrictions –
eg. restricted to types where suitable inversion principles apply. In
particular, existential variables of the instances of the parameters
(that is, the set of βi that appear in each τj) must not overlap –
this rules out the (('a,+'a) eq) example of Jeremy.

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?

On Sat, Feb 11, 2012 at 2:51 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2012/02/10, at 19:11, Gabriel Scherer wrote:
>
>> I've been playing with GADTs and noticed that the condition on
>> parameter variance is very restrictive.
>>
>> The two following examples fail:
>>
>>   type +_ const =
>>   | Const : int -> int expr
>>
>>   type +_ expr =
>>   | Const : 'a -> 'a expr
>>   | Prod : 'a expr * 'b expr -> ('a * 'b) expr
>>
>>   Error: In this GADT definition, the variance of some parameter
>>   cannot be checked
>>
>> I looked at the source, and this is what I could infer of the current
>> typer behavior: parameter variance check will fail (on non-invariant
>> parameters) as soon as they appear *instantiated* (not just
>> a variable) in one of the GADT branch return type. The two examples
>> above fail for this reason: `const` parameter is instantiated with int
>> and `expr` with ('a * 'b).
>>
>> Would it be possible to relax this condition a bit? Intuitively, I
>> would say that:
>> 1. variables that do not appear in the instantiations of the return
>>   type always satisfy their variance constraint (for the branch)
>> 2. variables that appear covariantly in the instantiations of the
>>   return type should satisfy their constraints on the argument types
>> 3. variables that appaear contravariantly should satisfy the
>>   *reversed* constraints on the argument type
>>
>> For example, with a GADT having some argument type σ('a) using
>> a variable instantiated in its return type :
>>
>>   type +_ t = | C : σ('a) -> ('a -> unit) t
>>
>> If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' →
>> unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a
>> appears *contravariantly* in σ.
>>
>> Is the above condition sound? It would allow my two examples above. If
>> not, or if it's not reasonable to implement, is there a weaker
>> condition that would make those example work?
>>
>> Having a powerful enough variance inference is important if we want to
>> use GADTs to implement abstract data types – that's how I ran into
>> this problem.
>
> As Jeremy pointed already, the question of variance in presence of GADTs
> is devilishly complicated.
> Your conditions are much too simple to be sufficient.
> They seem to be the conditions we already have for constrained types.
>
> I'm ready to buy anything, but at least I need a proof of soundness.
>
> At the very least, the conditions seem to be
> 1) an instantiated type cannot include type variables that appear elsewhere in the return type
>     (Jeremy's example)
> 2) if an instantiated type is marked as contravariant, it should not be possible to smuggle
>     a value of this type through the arguments
>     (the example in the ocamlgadt tutorial)
> 3) something similar for the contravariant case
>
> However this is completely unclear whether this would be sufficient.
>
> For your first example, the contravariant version is clearly unsound:
>
> type pint = private int
> type -_ const = Const : int -> int const
>
> let eval : type a. a t -> a = fun (Const c) -> c
> let make_pint (x : int) : pint = eval (Const x :> pint const)
>
> I think that your examples are ok, but I'm not sure how to generalize that.
>
>        Jacques Garrigue
>