Question on GADT and variance annotation

Learning
,
1

Dear all,

I don’t understand why the following type definition is not accepted:

type +_ u = U : 'a -> 'a list u
Error: In this GADT definition, the variance of some parameter
       cannot be checked

Could someone explain what’s going wrong here? Thanks!

2

To me it seems that 'a is contravariant but 'a list is covariant, which looks like conflicting variance requirements. And just to confirm, if we remove the variance annotation, the error goes away.

3

I don’t think that 'a appears in contravariant position here, because of two vague arguments:

  • if I transpose this example to regular ADT, it works:
type +'a t = U of 'a

(not sure though this analogy is worth something)

  • if I purposely put the variable in contravariant position I get an explicit error message:
type +_ t = U : ('a -> int) -> 'a t
Error: In this definition, expected parameter variances are not satisfied.
       The 1st type parameter was expected to be covariant,
       but it is injective contravariant.
4

And also:

type +_ t = U : 'a -> 'a t

works…

5

I think this is a limitation of the type checker. I agree that the type parameter is covariant because 'a list has the same variance as 'a and 'a is in a covariant position in U.

6

The variance of type parameters for GADTs is a far more complex question than for ordinary variants. In particular, the usual criteria that a type parameter which only appears in covariant positions is covariant is inapplicable.

Indeed, consider for instance,

type (_,_) eq = Eq: ('a,'a) eq

The two type parameters of eq only appear in covariant or contravariant positions (because they don’t appear at all). However, (< >, <x:int>) eq is not a subtype of (< x:int>, <x:int>) eq. In other words, eq must be invariant in its two type parameters.

Right now, to avoid this complexity the typechecker consider that for GADTs only type parameters that are never constrained (in other words maps exactly to ordinary variants) might be covariant or contravariant. For instance:

type (+'a,_) pair= P:'a * 'a -> ('a,int) pair;;

All other type parameters are considered invariant. Since your example is constraining the type parameter to _ list it falls in this category.

8 Likes
7

Cristal clear, thanks!

1 Like
8

In case one is really fixated on having the variance annotation, there is the following trick:

type _ u =
| Val : 'a -> 'a u
| Int : int -> int u
| Prod : 'a expr * 'b expr -> ('a * 'b) u

and +'a expr = Expr : 'b u * ('b -> 'a) -> 'a expr

The idea is to pack the original GADT with a coercion function that returns the exposed type variable. Since it appears only once and in a covariant position, the whole type is covariant.

In practice, this coercion is just the identity function, as can be seen from the following smart constructor definitions:

let value x = Expr (Val x, Fun.id)
let int i = Expr (Int i, Fun.id)
let prod x y = Expr (Prod (x, y), Fun.id)

J. Yallop and S. Dolan proposed a more elegant solution in their paper “First class subtypes”

https://www.cl.cam.ac.uk/~jdy22/papers/first-class-subtypes-draft.pdf

but their extension relies on module-dependent arrow (as in modular explicits). IIUC module-dependent arrows should not increase the expressiveness of the language, so maybe a translation to stock OCaml is possible.

1 Like