Covariance and Contravariance (computer Science) - Formal Definition

Formal Definition

Within the type system of a programming language, a typing rule or a type conversion operator is:

• covariant if it preserves the ordering, ≤, of types, which orders types from more specific to more generic;
• contravariant if it reverses this ordering, which orders types from more generic to more specific;
• invariant if neither of these applies.

These terms come from category theory, which has a general definition of covariance and contravariance that unifies the computer science definition of these terms with the definition used in vector spaces.

This distinction is important in considering argument and return types of methods in class hierarchies. In object-oriented languages such as Python, if class B is a subtype of class A, then all member functions of B must return the same or narrower set of types as A; the return type is said to be covariant. On the other hand, if the member functions of B take the same or broader set of arguments compared with the member functions of A, the argument type is said to be contravariant. The problem for instances of B is how to be perfectly substitutable for instances of A. The only way to guarantee type safety and substitutability is to be equally or more liberal than A on inputs, and to be equally or more strict than A on outputs. Note that not all programming languages guarantee both properties in every context, and that some are unnecessarily strict; they are said not to support covariance or contravariance in a given context; the behavior of some programming languages is discussed below.

Typical examples:

• The operator which constructs array types from element types is usually covariant on the base type: since String ≤ Object then ArrayOf(String) ≤ ArrayOf(Object). Note that this is only correct (i.e. type safe) if the array is immutable; if insert and remove operators are permitted, then the insert operator is covariant (e.g. one can insert a String into an ArrayOf(Object)) and the remove operator is contravariant (e.g. one can remove an Object from an ArrayOf(String)). Since the mutators have conflicting variance, mutable arrays should be invariant on the base type.
• Let f be a function with a parameter of type T and let g be a function with a parameter of type S, both with the same return type. If T ≤ S, then g ≤ f. g can replace f anywhere, since it cares less about the type of its parameter, and both return the same type. Because the subtype relation between the argument type and the functions is reversed, the function type is said to be contravariant on its argument type.
• Let f be a function that returns a value of type T and let g be a function that returns a value of type S, both with the same parameter type. If T ≤ S, then f ≤ g. f can replace g anywhere, since it returns only a subset of all possible values returned by g, and both take the same argument. Because the subtype relation between the argument type and the functions is preserved, the function type is said to be covariant on its return type.

In object-oriented programming, substitution is also implicitly invoked by overriding methods in subclasses: the new method can be used where the old method was invoked in the original code. Programming languages vary widely on their allowed forms of overriding, and on the variance of overridden methods' types.