In this second installment of the "toy type language" series, we will explain how to compute the variance of mutually recursive parameterized types. The actual implementation will be the topic of a following post.
The interest of variance is best seen in combination with a subtyping relation. We therefore assume a type system equipped with a subtyping relation which we write as
≤. In order to give meaningful examples of subtyping, I will use polymorphic variants, so that readers familiar with that feature of OCaml can follow the discussion easily.
The type of values that may only be the constructor
A, which OCaml can express as
[ `A ], is a subtype of the type made up of two constructors
[ `A | `B ]. We write this as
[ `A ] ≤ [ `A | `B ]: any inhabitant of the smaller type can be seen as an inhabitant of the bigger type. One can think in terms of sets, in which case
≤ is the set inclusion relation
Variance is a property of a parameterized type with regards to one of its parameters. If
t a is a parameterized type, the variance of
t with regards to
a will give us information about the kind of subtyping relation that two types
t a and
t b enjoy, depending on the subtyping relation between
Variance is especially important for abstract types. The definition of an abstract type is hidden; therefore, unless otherwise specified, no subtyping relations are available. However, we may want to reveal in a module's signature that a type has a certain variance, so that the type-checker be aware of certain subtyping relations. Therefore, variance is a property that we will sometimes want to export through a module signature.
The four possible variances
type 'a list = | Nil | Cons of 'a * 'a list
If we see
list as a function from types to types, then
list is nondecreasing: assuming
a ≤ b, we have
list a ≤ list b1. We say that
list is covariant in its first parameter. If the type
list were to be abstract, revealing that it is a covariant type would make sure the type-checker is aware that "
a ≤ b ⇒ list a ≤ list b".
type 'a printer = 'a -> unit
We now turn to the
printer type, which is that of a function that can print elements of type
'a. Intuitively, if a function can print elements with constructor
B, it can also print elements with only constructors
A: the function's
B case will just never be called. In other words, we can see a
printer [ `A | `B ] as a
printer [ `A ], which we write
printer [ `A | `B ] ≤ printer [ `A ]. This fact is true even though
[ `A ] ≤ [ `A | `B ]. This is the opposite of
printer is a nonincreasing function from types to types. We say that
printer is contravariant in its first parameter.
type 'a list_with_printer = 'a printer * 'a list
list_with_printer type is made up of a covariant type and a contravariant type;
list_with_printer is neither co- nor contravariant. We say that it is invariant, meaning the
list_with_printer does not enjoy any subtyping relation. This is the default variance: an abstract type is considered to be invariant by default.
type 'a t_bi = ()
A rarely useful variance is bivariance, when a type is both co- and contravariant. This is only possible if the type does not use its type parameter, such as
t_bi in the example above. Indeed, we always have both
t_bi a ≤ t_bi b and
t_bi b ≤ t_bi a for any
We now need to reveal the variance of an abstract type through a module signature, so that the type-checker can take advantage of this extra information. OCaml offers notation in module signatures for all variances, except bivariance.
module M: sig type +'a co_t type -'a contra_t type 'a inv_t end = struct type 'a co_t = 'a list type 'a contra_t = 'a printer type 'a inv_t = 'a printer * 'a list end
The variance lattice
Variance forms a complete lattice, which induces a "meet" ("goes down") and a "join" ("goes up") operation, which we respectively write as
inv / \ co contra \ / bi
We now turn to the actual process of computing variance. Let's assume first that a recursive procedure is enough to compute the variance of a given data type.
list_with_printer type. When trying to compute
variance(list_with_printer, a), we need to compute
variance(list, a) and
variance(printer, a). Assuming the variances for
printer have been computed already, we obtain
contra. Then, the variance of
list_with_printer is one that subsumes both the variance of
printer, as the two appear in the definition of
list_with_printer. Finding a variance that is greater than both
contra corresponds to a "join" operation on the lattice.
variance(list_with_printer, a) = variance(list, a) ∪ variance(printer, a) = co ∪ contra = inv
For the example above, a simple recursive computation may suffice. However, in the presence of recursion, computing the variance of
list requires that one knows the variance of
list already, as
list occurs in its own definition!
The variance for
list can be computed using a least fixed point: we initially assume the variance of
list to be the "best" possible (bivariant). Under this hypothesis, we compute the variance of
list, which turns out to be
We then perform a second iteration: assuming
list is now covariant, the computed variance for
list is still
co: we have reached a fixed point. Starting from the bottom of the lattice guarantees we reach the least fixed point: indeed, invariant is a valid fixed point for
list, but not the best (least) one.
We can sum up this procedure as follows, where the fixed point is not reached until the second line.
variance(list, a): bi ⊢ variance (list, a) = co variance(list, a): co ⊢ variance (list, a) = co
Systems of equations
We can express variance using a system of equations. Back to the
list_with_printer example, if
v is the variance associated to the parameter
list_with_printer, we write:
v = variance(list_with_printer, a)
How do we compute the variance? We look up the definition of
list_with_printer, and figure out that this type is defined to be a tuple. Computing variance for a tuple is easy; we just apply the "join" operation.
(* [variance t a] computes the variance of parameter [a] in type [t] *) variance :: type -> parameter -> variance variance((t, u), a) = variance (t, a) ∪ variance (u, a)
This reduces to:
v = co ∪ contra
Solving this equation is straightforward and the fixed-point computation is trivial:
inv is the least fixed point of that equation, therefore,
list_with_printer is invariant over its first parameter.
We have shown the definition of the
variance function in the case of tuples. Another easy case is that of a variable:
variance(a, a) = co variance(b, a) = bi
The variance of
a itself is covariant; the variance of
a in another, distinct type variable is
a does not appear in type
Arrow types are __contra__variant in their domain: if
a appears in covariant position in
a is __contra__variant in
t -> unit. We therefore introduce a negation operator, which we write
-, defined as follows:
-inv = inv -co = contra -contra = co -bi = bi
variance(t -> u, a) = - variance(t, a) ∪ variance (u, a)
We still haven't defined the
variance function in the case of type applications, which we write
t u. Computing the variance of
t u requires composing the variance of
t in its first parameter and the variance of
Still seeing data types as functions, this amounts to computing the monotonicity of the composition of two functions.
v is the variance of
t in its first parameter, and
w is the variance of
u, then we define
variance as follows:
variance(t u, a) = var_for_param(t, 0) . variance(u, a)
We compose the variance of
t in its first parameter with the variance of
How should we define the dot operator? Let us take some examples. If
variance(u, a) = w, then
variance(list u, a) remains
w: we say that
co.w = w. Conversely,
variance(printer u, a) is
-w: we have
contra.w = -w. An interesting case if that of bivariance: if
a does not appear in
a won't appear in
t u, meaning
v.bi = bi. Symmetrically, if
t does not use its parameter
a won't appear in
t u, meaning
bi.w = bi. Finally, composing an invariant type with any other type yields an invariant type.
The composition of
w, which we write as
v.w, is summed up in the following table.
This allows us to write the system of equations for the
v = (co ∪ v.co) ∪ bi
Mutually recursive data types
The fixed-point computation becomes much more interesting in the case of multiple, mutually recursive data types. Consider the following definition:
type ('a, 'b) t = | Foo of ('a -> 'b) | Bar of ('a * 'b, 'b) u and ('c, 'd) u = | Baz of ('c, 'c) t
The system of equations needs four variables,
vd which are the variances of all four type parameters.
va = -co ∪ bi ∪ vc.co ∪ vd.bi vb = -bi ∪ co ∪ vc.co ∪ vd.co vc = va.co ∪ vb.co vd = va.bi ∪ vb.bi
We have now explained how to write down the recursive equations that allow one to compute the variance of mutually recursive data types. The next and final blog post will show how to compute the least fixed point for any set of equations, using the
I am intentionally not using the OCaml notation here, but the more conventional one usually found in papers, where data types are treated just like functions applied to arguments.↩