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

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

Indeed, the (=) in my message above where in the context of the work
where it is define as ((<=) and (>=)), so in a sense "equality in the
sense of subtyping rather than unification". Sorry for the confusion.
I'll now mark this relation as <=>.

>> 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.
>
> I don't see why this could not be allowed without the restriction you
> propose. I thought that this was rejected in 4.00 because 4.00 used
> bi-variance as an (unsafe) approximation of non-injective. Since we now
> track injectivity separately from variance g be accepted (with 'a covariant).

In our work, this GADT definition would be accepted, and:
(1) matching on the constructor G does not give any information on the
value of the existential type 'a
(2) the parameter of g (not 'a, the one marked _ above) may marked
covariant or invariant, because the constructor t is upward-closed but
not downward-closed (private types)

In particular, the following does not type-check:
  let extract : int t g -> int = function
    | G n -> n

The G constructor at type ('b t) has type (exists 'a ['a t <=> 'b].
'a); so in the G branch the type-checker introduces the hypothesis ('a
t <=> int t) for an existential variable 'a. This does not allows to
deduce ('a <=> int) and therefore the body does not type-check.

However, in the OCaml type system, GADT type equalities are understood
in the unification sense (because it is the one that mixes well with
the inference engine), so the constructor G at type ('b g) would have
type (exists 'a. ['a t = 'b]), with (=) in the unification sense. As
Jacques said, this means that we must either reject the definition of
('b g) as is currently done, or stop considering ('a t) injective.

PS: Note that you could understand type parameter constraints in the
same way, which makes them safe without requiring injectivity, but
Didier remarked that this will only delay failure as code writers
generally assume injectivity. It's before to fail at definition site
than at usage site if you know you should fail anyway.

On Tue, Apr 30, 2013 at 12:12 PM, Leo White <lpw25@cam.ac.uk> wrote:
> [Sorry if this is a repeat post]
>
>> 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.
>
> I think Gabriel meant that 'a bivar = 'b bivar were equal in the
> subtyiping relationship, rather than in the unification
> relationship. (Perhaps we should use a different symbol for subtyping
> equality).
>
>> 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.
>
> I don't see how this implies the need for the strengthening you
> describe. As I see it:
>
>   type 'a t = T
>
> creates a type that is bi-variant in its parameter, so all occurences of
> 'a in:
>
>   type 'a u = 'a t -> 'a t
>
> are in bi-variant positions, so u should also be bi-variant.
>
>> 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.
>
> I don't see why this could not be allowed without the restriction you
> propose. I thought that this was rejected in 4.00 because 4.00 used
> bi-variance as an (unsafe) approximation of non-injective. Since we now
> track injectivity separately from variance g be accepted (with 'a covariant).