[Caml-list] Re: Variance of GADT parameters

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

On 2012/04/13, at 19:51, Gabriel Scherer wrote:

>>> 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...
> 
> Variance annotations on abstract types are already in the domain of
> experts library writers, not simple users – most people have never
> heard of them. I don't think the upward/downward closure criterion is
> much harder to understand or would have much cognitive burden.

Maybe they have never heard of them, but I believe variance annotations are really intuitive.
However, understanding upward/downward closure is another story.
Actually, this property itself seems in contradiction with subtyping:
it says that a type is outside of the subtyping hierarchy.
I understand that this may make some things easier (in relation with
subtyping), but I'm afraid you will end-up wanting it both inside and outside...

Moreover, if we add "blind" types, which would be needed for subtyping
constraints in GADTs, don't you end-up losing both closure properties
on all types?

>> What do you mean by "all reasonable variance properties" ?
>> This should only have an impact on GADTs, isn'it ?
> 
> I mean that upward-closure is currently a fairly natural notion for
> ordinary types (yes, if a tuple (x,y) can be given a type, then it
> must be a cartesian product type), which would be broken by adding
> those types. I informally and nearly unconsciously assumed it held
> when reasoning about my (Prod : α expr * β expr → (α * β) expr)
> constructor.
> 
> Yes, among the type-system features I know of, this would only impact
> GADTs. More precisely, that would only impact GADTs whose constraint
> are equality constraints. Still that is something to take into
> account. I suppose you were not aware, at the time of introducing
> private types, that this added feature could negatively impact other
> areas of the type system; we now have the opportunity to ponder this
> tension more carefully.
> 
> (I don't know which of GADTs or private types people would find more
> useful; that surely depends on one's domain and programming
> style. What would we do if we were given the opportunity to go back in
> time and remove private types to strengthen equality GADTs?)
> 
> I believe saying "this new type will never be made private in the
> future" is the good way to control this tension. I didn't like the
> idea at first, but that's a way to have our two cakes (private types
> and equality GADTs) and eat them both, without either one putrefying
> the other.

Let us not mix things up.
The tension is not between GADTs and private types, but between one
way to add variance annotations to GADTs and private types.
Since variance annotations are originally for subtyping, it is actually
a tension between two extensions to subtyping.
And I don't think that restricting subtyping is a good way to strengthen it :-)
So my intuition is that relying on upward/downward closure is fundamentally
wrong, because it restricts the subtyping relation you are allowed to use.

>> 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.
> 
> That is good news. I had not realized that, just as a local abstract
> types serves as existential variables, a local private type is in some
> way a "canonical" smaller type.

I forgot to mention that if we want both covariant and contravariant annotations,
we also need "blind" types...

>>> For example, the idiomatic use of the (+α expr) datatype is the
>>> (eval : ∀α. α expr → α) function, and it can be written on this
>>> monotonous version.
>> 
>> There are certainly examples in both directions.
>> For instance the "print" example in the manual uses the opposite direction.
> 
> There is a strong difference between the types "expr" and "ty"
> 
>  type α expr
>    | Val : α → α expr
>    | Prod : α expr * β expr -> (α * β) expr
> 
>  type α ty
>    | Ty : α expr
>    | Prod : α ty * β ty → (α * β) ty
> 
> `expr` carries data so is intuitively covariant. `ty` carries no data
> so could be used in either directions. Note that the printing function
> for `expr` does not require contravariance, as its type is
> `α expr → string`.
> 
> So I believe that the `print : α ty → α → string` is an example of
> GADT that should be invariant – rather than an example of GADT that we
> want to make covariant but couldn't this an open-world presentation,
> whatever that may mean.

OK, I understand better.
This seems to make sense.
Of course in many situations one would want equation constraints rather
than subtyping constraints, but this is really a choice about the semantics
of your type.

>> On the other hand, if you really want variance, this looks like a cleaner solution.
> 
> That's the idea. Having the option to use subtyping constraints rather
> than equality constraints would allow a library designer to make
> compromises. Invariance is easier to handle for everyone, but in case
> covariance is really important it can be done – which is not currently
> the case.
> 
> Note that the two ideas, one of using upward/downward closure to
> strengthen variance properties in the equality case, the other of
> using subtyping constraints to gain covariance at the cost of weaker
> elimination, are not mutually exclusive.

As I mentioned above, we would need "blind" types, which breaks upward closure.
Or is there a way out?

> I think a reasonable design process for a library writer would be to
> first go for the easy equality case and, if one discovers a need for
> {co,contra}variance, wonder about upward/downward closure properties
> and, if they don't hold, weaken the type to subtyping constraints in
> the good direction. Each step is potentially more expressive, but also
> more costly (in term of required annotations, etc.).

Actually, if variance is only obtained through subtyping constraints,
variance annotations could exactly mean that. I.e., you would just write

 type +_ expr =
   | Val : α → α expr
   | Prod : β*γ → β*γ expr
   | Priv : priv_int → priv_int expr

and it would automatically generate subtyping constraints for the relevant  cases.
(I.e. only the Prod and Priv cases)

I agree that code using this would still require much more type annotations.
If there are many applications for this, maybe we could infer simple cases of subtyping
(at least not to have to write the same annotation in each branch of the pattern matching)

Jacques Garrigue