In computer programming, type variance is the relationship between subtypes of a composite type (e.g. ) and the subtypes of its components (e.g. ). A language's chosen variance determines the relationship between, for example, a list of s and a list of s, or a function returning and a function returning .
If the type is a subtype of , then an expression of type should be substitutable wherever an expression of type is used. Depending on the variance of the type constructor, the subtyping relation of the simple types may be either preserved, reversed, or ignored for the respective complex types. In many programming languages, for example, "list of Cat" will be a subtype of "list of Animal", because the list type constructor is covariant. This means that the subtyping relation of the simple types is preserved for the complex types. On the other hand, "function from Animal to String" is a subtype of "function from Cat to String" because the function type constructor is contravariant in the parameter type. Here, the subtyping relation of the simple types is reversed for the complex types.
A programming language designer will consider variance when devising typing rules for language features such as arrays, inheritance, and generic datatypes. By making type constructors covariant or contravariant instead of invariant, more programs will be accepted as well-typed. On the other hand, programmers often find contravariance unintuitive, and accurately tracking variance to avoid runtime type errors can lead to complex typing rules.
In order to keep the type system simple and allow useful programs, a language may treat a type constructor as invariant even if it would be safe to consider it variant, or treat it as covariant even though that could violate type safety.
Formal definition
Suppose <code>A</code> and <code>B</code> are types, and <code><nowiki>I<U></nowiki></code> denotes application of a type constructor <code>I</code> with type argument <code>U</code>.
Within the type system of a programming language, a typing rule for a type constructor <code>I</code> is:
- covariant if it preserves the ordering of types (≤), which orders types from more specific to more generic: If <code>A ≤ B</code>, then <code>I<nowiki><A> ≤ I<B></nowiki></code>;
- contravariant if it reverses this ordering: If <code>A ≤ B</code>, then <code>I<nowiki><B> ≤ I<A></nowiki></code>;
- bivariant if both of these apply (i.e., if <code>A ≤ B</code>, then <code>I<nowiki><A> ≡ I<B></nowiki></code>);
- variant if covariant, contravariant or bivariant;
- invariant or nonvariant if not variant.
The article considers how this applies to some common type constructors.
C# examples
For example, in C#, if is a subtype of , then:
- is a subtype of . The subtyping is preserved because is covariant on .
- is a subtype of . The subtyping is reversed because is contravariant on .
- Neither nor is a subtype of the other, because is invariant on .
The variance of a C# generic interface is declared by placing the (covariant) or (contravariant) attribute on (zero or more of) its type parameters. The above interfaces are declared as , , and . Types with more than one type parameter may specify different variances on each type parameter. For example, the delegate type represents a function with a contravariant input parameter of type and a covariant return value of type . and C# deal with this by marking each array object with a type when it is created. Each time a value is stored into an array, the execution environment will check that the run-time type of the value is equal to the run-time type of the array. If there is a mismatch, an (Java) and further popularized in a paper by Luca Cardelli.
When dealing with functions that take functions as arguments, this rule can be applied several times. For example, by applying the rule twice, we see that <math>((P_1 \to R) \to R) \le ((P_2 \to R) \to R)</math> if <math>P_1 \le P_2</math>. In other words, the type <math>((A \to B) \to C)</math> is covariant in the position of <math>A</math>. For complicated types it can be confusing to mentally trace why a given type specialization is or isn't type-safe, but it is easy to calculate which positions are co- and contravariant: a position is covariant if it is on the left side of an even number of arrows applying to it.
Inheritance in object-oriented languages
In an object-oriented programming (OOP) language, when a subclass overrides a method in a superclass, the compiler must check that the overriding method has the right type. While some languages require that the type exactly matches the type in the superclass (invariance), it is also type safe to allow the overriding method to have a "better" type. By the usual subtyping rule for function types, this means that the overriding method should return a more specific type (return type covariance) and accept a more general argument (parameter type contravariance). In Unified Modeling Language (UML) notation, the possibilities are as follows (where Class B is the subclass that extends Class A which is the superclass):
<gallery perrow="5" heights="190" caption="Variance and method overriding: overview">
Image:Vererbung T.svg|Subtyping of the parameter/return type of the method.
Image:Inheritance_invariant.svg|Invariance. The signature of the overriding method is unchanged.
Image:Inheritance_covariant_return.svg|Covariant return type. The subtyping relation is in the same direction as the relation between ClassA and ClassB.
Image:Inheritance_contravariant_argument.svg|Contravariant parameter type. The subtyping relation is in the opposite direction to the relation between ClassA and ClassB.
Image:Inheritance_covariant_argument.svg|Covariant parameter type. Not type safe.
</gallery>
For a concrete example, suppose we are writing a class to model an animal shelter. We assume that is a subclass of , and that we have a base class (using Java syntax)
frameless|right|upright|alt=UML diagram
<syntaxhighlight lang="java">
class AnimalShelter {
Animal getAnimalForAdoption() {
// ...
}
void putAnimal(Animal animal) {
//...
}
}
</syntaxhighlight>
Now the question is: if we subclass , what types are we allowed to give to and ?
Covariant method return type
In a language which allows covariant return types, a derived class can override the method to return a more specific type:
thumb|right|upright|alt=UML diagram
<syntaxhighlight lang="java">
class CatShelter extends AnimalShelter {
Cat getAnimalForAdoption() {
return new Cat();
}
}
</syntaxhighlight>
Among mainstream OOP languages, Java, C++ and C# (as of version 9.0 ) support covariant return types. Adding the covariant return type was one of the first modifications of the C++ language approved by the standards committee in 1998. Scala and D also support covariant return types.
Contravariant method parameter type
Similarly, it is type safe to allow an overriding method to accept a more general argument than the method in the base class:
thumb|right|upright|alt=UML diagram
<syntaxhighlight lang="java">
class CatShelter extends AnimalShelter {
void putAnimal(Object animal) {
// ...
}
}
</syntaxhighlight>
Only a few object-oriented languages actually allow this (for example, Python when typechecked with mypy). C++, Java and most other languages that support overloading and/or shadowing would interpret this as a method with an overloaded or shadowed name.
However, Sather supported both covariance and contravariance. Calling convention for overridden methods are covariant with out parameters and return values, and contravariant with normal parameters (with the mode in).
Covariant method parameter type
A couple of mainstream languages, Eiffel and Dart allow the parameters of an overriding method to have a more specific type than the method in the superclass (parameter type covariance). Thus, the following Dart code would type check, with overriding the method in the base class:
thumb|right|upright|alt=UML diagram
<syntaxhighlight lang="dart">
class CatShelter extends AnimalShelter {
void putAnimal(covariant Cat animal) {
// ...
}
}
</syntaxhighlight>
This is not type safe. By up-casting a to an , one can try to place a dog in a cat shelter. That does not meet parameter restrictions and will result in a runtime error. The lack of type safety (known as the "catcall problem" in the Eiffel community, where "cat" or "CAT" is a Changed Availability or Type) has been a long-standing issue. Over the years, various combinations of global static analysis, local static analysis, and new language features have been proposed to remedy it, and these have been implemented in some Eiffel compilers.
Despite the type safety problem, the Eiffel designers consider covariant parameter types crucial for modeling real world requirements. Instead of defining , we define a parameterized class . (One drawback of this is that the implementer of the base class needs to foresee which types will need to be specialized in the subclasses.)
<syntaxhighlight lang="java">
class Shelter<T extends Animal> {
T getAnimalForAdoption() {
// ...
}
void putAnimal(T animal) {
// ...
}
}
class CatShelter extends Shelter<Cat> {
Cat getAnimalForAdoption() {
// ...
}
void putAnimal(Cat animal) {
// ...
}
}
</syntaxhighlight>
Similarly, in recent versions of Java the interface has been parameterized, which allows the downcast to be omitted in a type-safe way:
<syntaxhighlight lang="java">
class RationalNumber implements Comparable<RationalNumber> {
int numerator;
int denominator;
// ...
public int compareTo(RationalNumber otherNum) {
return Integer.compare(numerator * otherNum.denominator,
otherNum.numerator * denominator);
}
}
</syntaxhighlight>
Another language feature that can help is multiple dispatch. One reason that binary methods are awkward to write is that in a call like , selecting the correct implementation of really depends on the runtime type of both and , but in a conventional OO language only the runtime type of is taken into account. In a language with Common Lisp Object System (CLOS)-style multiple dispatch, the comparison method could be written as a generic function where both arguments are used for method selection.
Giuseppe Castagna observed that in a typed language with multiple dispatch, a generic function can have some parameters which control dispatch and some "left-over" parameters which do not. Because the method selection rule chooses the most specific applicable method, if a method overrides another method, then the overriding method will have more specific types for the controlling parameters. On the other hand, to ensure type safety the language still must require the left-over parameters to be at least as general. Using the previous terminology, types used for runtime method selection are covariant while types not used for runtime method selection of the method are contravariant. Conventional single-dispatch languages like Java also obey this rule: only one argument is used for method selection (the receiver object, passed along to a method as the hidden argument ), and indeed the type of is more specialized inside overriding methods than in the superclass.
Castagna suggests that examples where covariant parameter types are superior (particularly, binary methods) should be handled using multiple dispatch; which is naturally covariant.
However, most programming languages do not support multiple dispatch.
Summary of variance and inheritance
The following table summarizes the rules for overriding methods in the languages discussed above.
{| class="wikitable" border="1"
|-
! !! Parameter type !! Return type
|-
| C++ (since 1998), Java (since J2SE 5.0), D, C# (since C# 9) || Invariant || Covariant
|-
| C# (before C# 9) || Invariant || Invariant
|-
| Sather || Contravariant || Covariant
|-
| Eiffel || Covariant || Covariant
|}
Generic types
In programming languages that support generics (a.k.a. parametric polymorphism), the programmer can extend the type system with new constructors. For example, a C# interface like makes it possible to construct new types like or . The question then arises what the variance of these type constructors should be.
There are two main approaches. In languages with declaration-site variance annotations (e.g., C#), the programmer annotates the definition of a generic type with the intended variance of its type parameters. With use-site variance annotations (e.g., Java), the programmer instead annotates the places where a generic type is instantiated.
Declaration-site variance annotations
The most popular languages with declaration-site variance annotations are C# and Kotlin (using the keywords and ), and Scala and OCaml (using the keywords and ). C# only allows variance annotations for interface types, while Kotlin, Scala and OCaml allow them for both interface types and concrete data types.
Interfaces
In C#, each type parameter of a generic interface can be marked covariant (), contravariant (), or invariant (no annotation). For example, we can define an interface of read-only iterators, and declare it to be covariant (out) in its type parameter.
<syntaxhighlight lang="csharp">
interface IEnumerator<out T>
{
T Current { get; }
bool MoveNext();
}
</syntaxhighlight>
With this declaration, will be treated as covariant in its type parameter, e.g. is a subtype of .
The type checker enforces that each method declaration in an interface only mentions the type parameters in a way consistent with the / annotations. That is, a parameter that was declared covariant must not occur in any contravariant positions (where a position is contravariant if it occurs under an odd number of contravariant type constructors). The precise rule is that the return types of all methods in the interface must be valid covariantly and all the method parameter types must be valid contravariantly, where valid S-ly is defined as follows:
- Non-generic types (classes, structs, enums, etc.) are valid both co- and contravariantly.
- A type parameter is valid covariantly if it was not marked , and valid contravariantly if it was not marked .
- An array type is valid S-ly if is. (This is because C# has covariant arrays.)
- A generic type is valid S-ly if for each parameter ,
- Ai is valid S-ly, and the ith parameter to is declared covariant, or
- Ai is valid (not S)-ly, and the ith parameter to is declared contravariant, or
- Ai is valid both covariantly and contravariantly, and the ith parameter to is declared invariant.
As an example of how these rules apply, consider the interface.
<syntaxhighlight lang="csharp">
interface IList<T>
{
void Insert(int index, T item);
IEnumerator<T> GetEnumerator();
}
</syntaxhighlight>
The parameter type of must be valid contravariantly, i.e. the type parameter must not be tagged . Similarly, the result type of must be valid covariantly, i.e. (since is a covariant interface) the type must be valid covariantly, i.e. the type parameter must not be tagged . This shows that the interface is not allowed to be marked either co- or contravariant.
In the common case of a generic data structure such as , these restrictions mean that an parameter can only be used for methods getting data out of the structure, and an parameter can only be used for methods putting data into the structure, hence the choice of keywords.
Data
C# allows variance annotations on the parameters of interfaces, but not the parameters of classes. Because fields in C# classes are always mutable, variantly parameterized classes in C# would not be very useful. But languages which emphasize immutable data can make good use of covariant data types. For example, in all of Scala, Kotlin and OCaml the immutable list type is covariant: <syntaxhighlight lang="scala" inline>List[Cat]</syntaxhighlight> is a subtype of <syntaxhighlight lang="scala" inline>List[Animal]</syntaxhighlight>.
Scala's rules for checking variance annotations are essentially the same as C#'s. However, there are some idioms that apply to immutable datastructures in particular. They are illustrated by the following (excerpt from the) definition of the <syntaxhighlight lang="scala" inline>List[A]</syntaxhighlight> class.
<syntaxhighlight lang="scala">
sealed abstract class List[+A] extends AbstractSeq[A] {
def head: A
def tail: List[A]
/** Adds an element at the beginning of this list. */
def ::[B >: A] (x: B): List[B] =
new scala.collection.immutable.::(x, this)
/** ... */
}
</syntaxhighlight>
First, class members that have a variant type must be immutable. Here, <syntaxhighlight lang="scala" inline>head</syntaxhighlight> has the type <syntaxhighlight lang="scala" inline>A</syntaxhighlight>, which was declared covariant (<syntaxhighlight lang="scala" inline>+</syntaxhighlight>), and indeed <syntaxhighlight lang="scala" inline>head</syntaxhighlight> was declared as a method (<syntaxhighlight lang="scala" inline>def</syntaxhighlight>). Trying to declare it as a mutable field (<syntaxhighlight lang="scala" inline>var</syntaxhighlight>) would be rejected as type error.
Second, even if a data structure is immutable, it will often have methods where the parameter type occurs contravariantly. For example, consider the method <syntaxhighlight lang="scala" inline>::</syntaxhighlight> which adds an element to the front of a list. (The implementation works by creating a new object of the similarly named class <syntaxhighlight lang="scala" inline>::</syntaxhighlight>, the class of nonempty lists.) The most obvious type to give it would be
<syntaxhighlight lang="scala">
def :: (x: A): List[A]
</syntaxhighlight>
However, this would be a type error, because the covariant parameter <syntaxhighlight lang="scala" inline>A</syntaxhighlight> appears in a contravariant position (as a function parameter). But there is a trick to get around this problem. We give <syntaxhighlight lang="scala" inline>::</syntaxhighlight> a more general type, which allows adding an element of any type <syntaxhighlight lang="scala" inline>B</syntaxhighlight>
as long as <syntaxhighlight lang="scala" inline>B</syntaxhighlight> is a supertype of <syntaxhighlight lang="scala" inline>A</syntaxhighlight>. Note that this relies on <syntaxhighlight lang="scala" inline>List</syntaxhighlight> being covariant, since
<syntaxhighlight lang="scala" inline>this</syntaxhighlight> has type <syntaxhighlight lang="scala" inline>List[A]</syntaxhighlight> and we treat it as having type <syntaxhighlight lang="scala" inline>List[B]</syntaxhighlight>. At first glance it may not be obvious that the generalized type is sound, but if the programmer starts out with the simpler type declaration, the type errors will point out the place that needs to be generalized.
Inferring variance
It is possible to design a type system where the compiler automatically infers the best possible variance annotations for all datatype parameters. However, the analysis can get complex for several reasons. First, the analysis is nonlocal since the variance of an interface depends on the variance of all interfaces that mentions. Second, in order to get unique best solutions the type system must allow bivariant parameters (which are simultaneously co- and contravariant). And finally, the variance of type parameters should arguably be a deliberate choice by the designer of an interface, not something that just happens.
For these reasons most languages do very little variance inference. C# and Scala do not infer any variance annotations at all. OCaml can infer the variance of parameterized concrete datatypes, but the programmer must explicitly specify the variance of abstract types (interfaces).
For example, consider an OCaml datatype which wraps a function
<syntaxhighlight lang="ocaml">
type ('a, 'b) t = T of ('a -> 'b)
</syntaxhighlight>
The compiler will automatically infer that is contravariant in the first parameter, and covariant in the second. The programmer can also provide explicit annotations, which the compiler will check are satisfied. Thus the following declaration is equivalent to the previous one:
<syntaxhighlight lang="ocaml">
type (-'a, +'b) t = T of ('a -> 'b)
</syntaxhighlight>
Explicit annotations in OCaml become useful when specifying interfaces. For example, the standard library interface for association tables include an annotation saying that the map type constructor is covariant in the result type.
<syntaxhighlight lang="ocaml">
module type S =
sig
type key
type (+'a) t
val empty: 'a t
val mem: key -> 'a t -> bool
...
end
</syntaxhighlight>
This ensures that e.g. is a subtype of .
Use-site variance annotations (wildcards)
One drawback of the declaration-site approach is that many interface types must be made invariant. For example, we saw above that needed to be invariant, because it contained both and . In order to expose more variance, the API designer could provide additional interfaces which provide subsets of the available methods (e.g. an "insert-only list" which only provides ). However this quickly becomes unwieldy.
Use-site variance means the desired variance is indicated with an annotation at the specific site in the code where the type will be used. This gives users of a class more opportunities for subtyping without requiring the designer of the class to define multiple interfaces with different variance. Instead, at the point a generic type is instantiated to an actual parameterized type, the programmer can indicate that only a subset of its methods will be used. In effect, each definition of a generic class also makes available interfaces for the covariant and contravariant parts of that class.
Java provides use-site variance annotations through wildcards, a restricted form of bounded existential types. A parameterized type can be instantiated by a wildcard together with an upper or lower bound, e.g. or . An unbounded wildcard like is equivalent to . Such a type represents for some unknown type which satisfies the bound. This design works well with declaration-site annotations, but the large number of interfaces carry a complexity cost for clients of the library. And modifying the library interface may not be an option—in particular, one goal when adding generics to Java was to maintain binary backwards compatibility.
On the other hand, Java wildcards are themselves complex. In a conference presentation Joshua Bloch criticized them as being too hard to understand and use, stating that when adding support for closures "we simply cannot afford another wildcards". Early versions of Scala used use-site variance annotations but programmers found them difficult to use in practice, while declaration-site annotations were found to be very helpful when designing classes. Later versions of Scala added Java-style existential types and wildcards; however, according to Martin Odersky, if there were no need for interoperability with Java then these would probably not have been included.
Ross Tate argues that part of the complexity of Java wildcards is due to the decision to encode use-site variance using a form of existential types. The original proposals used special-purpose syntax for variance annotations, writing instead of Java's more verbose .
Since wildcards are a form of existential types they can be used for more things than just variance. A type like ("a list of unknown type") lets objects be passed to methods or stored in fields without exactly specifying their type parameters. This is particularly valuable for classes such as where most of the methods do not mention the type parameter.
However, type inference for existential types is a difficult problem. For the compiler implementer, Java wildcards raise issues with type checker termination, type argument inference, and ambiguous programs. In general it is undecidable whether a Java program using generics is well-typed or not, so any type checker will have to go into an infinite loop or time out for some programs. For the programmer, it leads to complicated type error messages. Java type checks wildcard types by replacing the wildcards with fresh type variables (so-called capture conversion). This can make error messages harder to read, because they refer to type variables that the programmer did not directly write. For example, trying to add a to a will give an error like
method List.add (capture#1) is not applicable
(actual argument Cat cannot be converted to capture#1 by method invocation conversion)
where capture#1 is a fresh type-variable:
capture#1 extends Animal from capture of ? extends Animal
Since both declaration-site and use-site annotations can be useful, some type systems provide both.