[Caml-list] Re: Variance of GADT parameters

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

Dear Gabriel,

Thank you for this detailed analysis.
It is comforting to know that the current criterion is sound!

I have a few remarks/questions.

> # A criterion in the general case
> 
> I believe (and have a draft of proof in the attached technical annex)
> that the requirement of Simonet&Pottier is equivalent, in the equality
> case, to the following criterion that *could* be implemented in
> a type-checker – more easily than by adding a general constraint
> solver.
> 
>  Given variance annotations (≤i) for the type ᾱ t, the type
>  constructor
>    K : ∀ᾱ∀β̄[α₁ = T₁(β̄), α₂ = T₂(β̄)...] τ̄ → ᾱ t
>  or equivalently (in OCaml syntax)
>    K : τ̄ → (T₁(β̄),T₂(β̄)...) t
>  respects the variance if all the conditions below are met:
> 
>  1. Non-interference: if an existential variable β appears in several
>     Ti(β̄), then all its occurences in the whole type expression
>     (T₁(β̄),T₂(β̄)...) t must be in invariant position.
> 
>  2. Upward/downward closure, or eliminability: for each i, β̄, α', if
>     (Ti(β̄) ≤i α') holds then α' is of the form Ti(β̄').
> 
>  3. Constructor parameters variance: the variance of the β̄ in the
>     type expression (T₁(β̄),T₂(β̄)...) t must respect their variance in
>     the constructor parameters τ̄ – just like if we had a non-GADT
>     declaration in term of the β̄, (type β̄ t = K of τ̄ | ...).
> 
> I believe this is sound, not unreasonably difficult to check, and
> would help in a lot of concrete cases that are currently rejected.

Have you considered my comment on the interaction with abstraction:

>> Again I wonder whether you are not going to get problems with abstraction.
>> At first sight, no: if when you define a GADT t, the type u is abstract, then
>> it will have no supertype in any environment where we use t.
>> But if you think more carefully, you realize that if in the future we allow
>> (gadt-)unification between abstract types, everything breaks, since abstract
>> types may end up having supertypes in a local environment.
>> So it looks like the only types you can allow for instantiation are concrete
>> datatypes and well-known types (abstract types defined in the initial environment
>> or in the current module).

In the future, we really want to be able to instantiate normal abstract types with
GADT pattern matching, not just local ones.
Wouldn't it mean that you can never now whether an abstract type is upward closed?

module M : sig type t type u = private int val eq : (t,u) eq end =
  struct type u = int  type t = u  let eq : (t,u) eq = Eq end

Note that this doesn't means that I could build a proof of unsoundness.
You criterion may actually be too restrictive.
Actually, my counter-example with a private type used a contravariant gadt.

> # Discussion of private types and contravariance
> 
> There is something quite disturbing in the idea that the mere
> existence of private types creates a strong asymmetry between
> covariant and contravariant parameters for GADTs: while upward-closed
> types are relatively common (so that we can expect "the usual
> examples" of GADTs to have "the expected variance"), there are no more
> downward-closed types, which means no contravariant constrained
> parameter.
> 
> Upward or downward closure can be easily decided on fully transparent
> types (types whose definition is known). But there is a problem with
> opaque types: as we don't know how they were defined, we can't check
> if they are upward/downward closed.

Sorry about the above comment.
This seems to be what you are referring to here.
I would just remind you that we have lots of opaque types around,
so that this may be a strong limitation in practice.
Of course we can still apply the criterion that opaque types in
the initial environment (builtin + pervasives) cannot be circumvented,
but this a kind of hack.

A stronger approach would be to check interfaces to ensure that abstraction
cannot be broken.
I was already thinking about that for making abstract types covariant when
the module interface only allows covariant uses.
But this can be very tricky.

> From a design point of view, the "right thing" would be to let people
> publish this information in the signature for an opaque type. Just as
> we can annotate the type with variance information, we should be able
> to publish its upward/downward closure properties.

This is rather heavy-weight...

> Another natural question is: what if we added the symmetric of the
> "private" concept, a type (blind σ) strictly above σ for all types?
> Would we lose all reasonable variance properties on OCaml types?

Is there any use for these "blind" types ?
What do you mean by "all reasonable variance properties" ?
This should only have an impact on GADTs, isn'it ?

> One idea from Didier Rémy is to allow, when defining a new type 't'
> (not a type synonym), to define it as "non-privatizable"
> (and correspondingly non-blindable). We or another programmer would
> then not be allowed to define a type 'private t'. In exchange for this
> lost flexibility, 't' would be downward-closed. The idea is that
> introducing private types increased our freedom, and reciprocally
> lessened our ability to reason about "what cannot be done";
> non-privatizable annotations allow to locally make the inverse choice
> of losing 'private' for better subtyping properties.

This one would really go against abstraction...

> From a pragmatic standpoint, I suspect the current restrictions
> 'private' entails on the GADT variance checks are not going to be
> really problematic in practice. We tend to use covariant types
> (data) more often than contravariant types (computations). The OCaml
> type system is already skewed towards covariance in one place: while
> the relaxed value restriction (which, I recall, is the reason why
> I needed GADT variance in the first place) would work equally well
> to generalize variables that appear only in covariant or only in
> contravariant positions, the relaxation is implemented in the
> type-checker only for covariant parameters. And I have not yet heard
> of someone requesting generalization of only-contravariant
> parameters, so apparently treating contravariant parameters as
> second-class citizens is ok among OCaml users.

Contravariant parameters are not generalized because this would
be unsound:

let f : 'a -> unit = let r = ref [| |] in
  fun x -> if !r = [| |] then r := [|x|] else (!r).(0) <- x

let crash = f 1.0; f 1

It is unsound to add a top type to the ocaml type hierarchy.
But the "blind" types would of course be sound.

> # A theoretical open-world approach
> 
> Some people may consider the upward-downward criterion as
> fundamentally unsatisfying because of the closed-world assumption it
> makes: it is not preserved by enrichment of the OCaml subtyping
> lattice.
> 
> There is another possibility to get some variance properties out of
> GADTs that still works in an open-world system: allow GADTs
> constraints to have subtyping constraints, instead of only equality
> constraint.
> 
> For example we could define the type of well-typed expressions in
> this way (note the ≥ in constraints):
>  type +α expr =
>    | Val : ∀α. α → α expr
>    | Prod : ∀α∀βγ[α ≥ β*γ] β*γ → α expr
>    | Priv : ∀α[α ≥ priv_int] priv_int → α expr
> 
> It is trivial that this definition is covariant in its type parameter,
> because covariance was baked in the definition. Indeed, if α≤α'
> and α≥β*γ, then α'≥β*γ by transitivity: the constraint is preserved by
> going to a larger type. In the soundness requirement of
> Simonet&Pottier, one can use the exact same existential variables on
> both sides (β̄':=β̄), and the constraints will be satisfied.
> 
> The downside of this easier covariance property is that we get weaker
> types on deconstruction (pattern matching of GADT values): when
> matching on a (α t), in the Prod clause, we only know that (α ≥ β*γ)
> rather than (α = β*γ) – note that we could regain the stronger
> hypothesis by locally using the closed-world assumption.
> 
> This simple idea has two potential problems:
> 
> 1. This may not be implementable as part of the current OCaml
>   type-checker, which uses type equalities internally and has more
>   limited subtyping support (in particular we can't abstract over
>   arbitrary subtyping assumptions). That said, this particular way of
>   adding subtyping hypothesis in the context might be simple enough
>   for it to handle.
> 
> 2. Getting a weaker hypothesis may be unusable: maybe the usual GADT
>   programs really make use of the equality assumptions, and going for
>   subtyping assumptions would make untypable programs that would be
>   perfectly fine under the closed-world assumption.
> 
> 
> Jacques can tell us about point 1.

This does not seem particularly difficult: we already extend the type environment
for GADTs, so it would only mean using private or "blind" types in place of
aliases.

> Regarding point 2., I'm not sure
> and have not thoroughly checked examples, but my intuition is that it
> is actually not a problem. I think that the types we naturally want to be
> covariant are also the types we want to manipulate as data (so it's ok
> if the type is larger than what we expect), rather than consumers, and
> conversely.
> 
> For example, the idiomatic use of the (+α expr) datatype is the
> (eval : ∀α. α expr → α) function, and it can be written on this
> monotonous version.
> 
> let rec eval : ∀α. α expr → α = function
>  | Val (v : α)                        → (v : α)
>  | Prod ∃βγ[α≥β*γ] (b:β, c:γ)        → ((b, c) : β*γ :> α)
>  | Priv [α ≥ priv_int] (n : priv_int) → (n : priv_int :> α)
> 
> One would need to study more examples to get a better understanding of
> this question.

There are certainly examples in both directions.
For instance the "print" example in the manual uses the opposite direction.
And in some cases you are going to want both simultaneously.
Moreover this is very heavy: all subtyping requires type annotations,
while type equalities are directly handled by unification.
This may look like you don't need that many here, but in general
we only currently require type annotations on ambiguous types
when they escape the current case. In some cases this is a tiny
fraction of the uses of equality.

On the other hand, if you really want variance, this looks like a cleaner solution.

> # Conclusion and questions
> 
> We have a relaxed criterion that we're confident is sound and can
> plausibly be implemented in OCaml (including possibly before the
> next release). But it relies on a closed-world assumption that is
> currently skewed towards covariance because of private types -- not
> a problem for our use case, the relaxed value restriction. Finally, it
> would suggest some language extensions to benefit fully from it, by
> enabling upward/downward closure specification for abstract types, and
> allowing to forbid making a new type `private` in the future
> (or blind) to gain stronger variance properties.
> 
> On the other hand, we know that this criterion would not hold as is in
> an open world scenario. Is this consideration relevant to the OCaml
> type system? If one wants to keep the door open to the open world
> case, would the suggested approach (reasoning under subtyping
> constraints in pattern clauses) be implementable?

For OCaml the problem is abstraction.
I think it has consequences very close to open world, except if you're
willing to add lots of information to interfaces.

> I don't believe the two choices are exclusive: if we have an
> annotation to say "this type will never be marked private", it becomes
> downward-closed even in an open-world scenario, and we can recover the
> current behavior by saying that all types, by default, "will never be
> marked blind" but "may be marked private". Those defaults are design
> areas to explore.
> 
> I would welcome feedback on the current state of affairs. Given what
> we know, is there a hope of relaxing the variance check for GADT at
> some short-to-medium-term point?

Well, your simplest criterion (just check that the instantiated parameter
is upward-closed, failing on "unknown" abstract types) seems easy enough to check.
The question is whether is it really sufficient in practice.
For all the other annotations, there would need to be a very strong justification.
Honestly, my feeling is just that GADTs do not play well with subtyping, and
there is no really satisfactory solution (except maybe subtyping constraints, but
they are going to be very heavy).

	Jacques Garrigue