Covariance and contravariance

Covariance and contravariance are fundamental concepts in the field of type theory and category theory, which are branches of mathematics and computer science. These concepts describe how the types of objects and functions change in response to transformations in their input and output types.

Covariance

In type theory, a type constructor is said to be covariant if it preserves the order of types. This means that if type A is a subtype of type B, then the constructed type F(A) is a subtype of F(B). Covariance is often encountered in the context of object-oriented programming and generic programming.

For example, in a programming language with inheritance, if class Dog is a subclass of class Animal, then an array of Dogs can be considered a subtype of an array of Animals. This is because the array type constructor is covariant.

Contravariance

Contravariance is the opposite of covariance. A type constructor is contravariant if it reverses the order of types. In other words, if type A is a subtype of type B, then the constructed type F(B) is a subtype of F(A).

Contravariance is often used in the context of function types. For instance, if a function type takes an argument of type A and returns a result of type B, then a function that takes an argument of type B and returns a result of type A can be considered a subtype of the original function type. This is because the function type constructor is contravariant in its argument type and covariant in its return type.

Invariance

A type constructor is said to be invariant if it does not exhibit either covariance or contravariance. This means that there is no subtype relationship between the constructed types, regardless of the subtype relationship between the original types.

Applications

Covariance and contravariance are crucial in the design of type systems for programming languages. They help ensure type safety and enable more flexible and reusable code. These concepts are also important in category theory, where they relate to the behavior of functors and natural transformations.

Related Concepts

• Type theory
• Category theory
• Object-oriented programming
• Generic programming
• Inheritance (object-oriented programming)
• Function type
• Type safety
• Functor
• Natural transformation

See Also

• Polymorphism (computer science)
• Subtyping
• Type constructor
• Type system
• Variance (computer science)