The type system of many programming languages supports subtyping. For instance, if Cat
is subtype of Animal
, then an expression of type Cat
can be used whenever an expression of type Animal
could. Variance refers to how subtyping between more complex types (list of Cat
s versus list of Animal
s, function returning Cat
versus function returning Animal
, ...) relates to subtyping between their components. Depending on the variance of the type constructor, the subtyping relation may be either preserved, reversed, or ignored. For example in OCaml, "list of Cat" is a subtype of "list of Animal" because the list constructor is covariant, while "function from Animal to String" is a subtype of "function from Cat to String" because the function type constructor is contravariant in the argument type.
A programming language designer will consider variance when devising typing rules for e.g. 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 when that can violate type safety.
Within the type system of a programming language, a typing rule or a type constructor is:
The article considers how this applies to some common type constructors.
For example in C#, if Cat
is a subtype of Animal
, then: