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

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

> 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).

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?

On Tue, Apr 30, 2013 at 10:18 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2013/04/30, at 17:02, Alain Frisch <alain@frisch.fr> wrote:
>
>> On 04/30/2013 09:56 AM, Jacques Garrigue wrote:
>>> On 2013/04/30, at 15:59, Alain Frisch <alain@frisch.fr> wrote:
>>>
>>>> It's reassuring to see that the conservative solution (not assuming injectivity of user defined abstract types) does not seem too bad for now, even if not very satisfying.
>>>>
>>>> I'm only concerned with:
>>>>
>>>>> 3) The problem I describe in my first mail. I.e. when defining a type,
>>>>>   if you use type variables appearing in constrained type parameters,
>>>>>   you need the type constructors leading to the type variables to be
>>>>>   injective. This is PR#5985, and it is only fixed in branches/non-vanishing.
>>>>
>>>> Do you think that fixing this unsoundness (without injectivity annotations) would lead to reject existing programs?
>>>
>>> Potentially yes.
>>> But I don't know how it is in practice for code existing now.
>>> Hence my question.
>>
>> Apart from GADTs, does your patch address the unsoundness with type constraints?
>
> Sure, this is exactly the same mechanism.
>
> 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.
>
> Jacques Garrigue
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs