Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs

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

On 2013/04/30, at 18:11, Gabriel Scherer <gabriel.scherer@gmail.com> wrote:

>> The only other thing it does is a slight strengthening of variance checking.
>> 
>> Consider the type
>>   type 'a t = T                   (* 'a bi-variant and injective *)
>>   type 'a u = 'a t -> 'a t    (* 'a t occurs both at positive and negative positions *)
>> 
>> Originally, the parameter of u would have been bi-variant (or unrestricted)
>> since it is bi-variant in the definition of t.
>> However it is now invariant.
>> The reason is that you can only change it by subtyping in t, and u doesn't allow subtyping.
>> This is a reasonable restriction, and it is necessary to allow some GADT
>> definitions where we use concrete types as indices.
> 
> I'm not sure about this. In our work on variance of GADTs (
> http://arxiv.org/abs/1301.2903 ), we defined equality exactly as the
> antisymmetric closure of the subtyping relation (as is done in the
> previous work by Simonet and Pottier), and all type constructors are
> functional: (a = b) implies (a t = b t). This means that in our
> formalization, you ('a u = 'a bivar -> 'a bivar) is bivariant, because
> ('a bivar = 'b bivar) for any 'a and 'b implies (a u = 'a bivar -> 'a
> bivar = 'b bivar -> 'b bivar = 'b u).
> 
> This vision of invariance as still functional also plays nicely with
> the inversion principle: when you have (a t <= b t) when t covariant,
> you can deduce (a <= b), when t is contravariant you have (a >= b),
> and we can explain invariance as saying that you then have both, (a <=
> b) and (b <= a), which coincides with the algorithmic notion of
> "occurs both negatively and positively". The nice thing is that this
> inversion criterion is also complete, from (a <= b) and (b <= a) you
> can deduce (a t <= b t) for t invariant (in our system).

But it seems to me that this contradicts the definition of injectivity.
Namely, if we follow your definition, and have 'a bivar = 'b bivar, then
clearly bivar is not injective.
So there are two solutions: either we do not allow a bi-variant type
to be injective (breaking our simple statement that concrete types
are injective in all their parameters), or we consider bi-variance +
injectivity is some intermediary state, where we can use both directions
of subtyping, but not strong (unification) equality.

> What is the reason for adding your strengthening? What I understood so
> far is that unification, and therefore provable equality/inequalities,
> were orthogonal to variance (eg. (type 'a t = T) is both bivariant and
> injective). Is there a reason to tie them back together precisely in
> the invariant case?


The theoretical reason is above.
The practical reason is to make easier to define indices.
If we keep the bi-variance in an invariant context, then the following
type definition is refused:

	type 'a t = T;;
	type _ g = G : 'a -> 'a t g;;

In 4.00, this definition is refused because 'a in 'a t g is bi-variant, but 'a appears
in a covariant position.

Jacques Garrigue