[Caml-list] Re: Variance of GADT parameters

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

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