3 ms·

Why are covariance and contravariance important, and how do their type theory definitions differ from mathematical or statistical definitions of covariance and

Why are covariance and contravariance important, and how do their type theory definitions differ from mathematical or statistical definitions of covariance and contravariance? Is it just a distinction of which direction the type hierarchy flows, and the consequences that must have with regard to functions in order for logical consistency to be maintained?

solipsism 9y ago
The reason anyone cares is because we want static and yet flexible typing. The better a type system understands covariance and contravariance, the better it can be at statically checking complex relationships.
ufo 9y ago
You are getting the right idea there. It all has to do with how the typing rules look like in programming languages with subtyping. In a type system with subtyping, having a type A be a subtype of a type B (A <: B) means that we can pass a value of type A to any place where a value of type B would be expected. For basic types, the subtyping rules are pretty simple: just follow the class definition hierarchy. a Dog is an Animal, an Animal is an Object, and so on. For parameterized types, like collections (List[X]) or functions (Function[A,B]), it is a bit more complicated. The only way to go is to define the subtyping rule for T[X] in terms of the subtyping rule for X but which rule do we use? - T[A] <: T[B] iff A <: B ? (covariance) - T[A] <: T[B] iff A :> B ? (contravariance) - T[A] <: T[B] iff A = B ? (invariance) Well, it depends on the type! For example, function types (A->B) are contravariant with respect to the input type (the As) and covariant with respect to the output types (the Bs). For collections it depends on what operations are allowed. Read-only collections are covariant, write-only collections are contravariant and read-write collections are invariant. This last part is where knowing about variance becomes important for programmers. When it comes to user-defined parameterized types, the variance rules are different so to find out if a given type is covariant, contravariant or invariant the only option is to read the type annotations and documentation. And you also need to know what variance is to understand those annotations when you come across them.

solipsism 9y ago

The reason anyone cares is because we want static and yet flexible typing. The better a type system understands covariance and contravariance, the better it can be at statically checking complex relationships.

ufo 9y ago

You are getting the right idea there. It all has to do with how the typing rules look like in programming languages with subtyping. In a type system with subtyping, having a type A be a subtype of a type B (A <: B) means that we can pass a value of type A to any place where a value of type B would be expected. For basic types, the subtyping rules are pretty simple: just follow the class definition hierarchy. a Dog is an Animal, an Animal is an Object, and so on. For parameterized types, like collections (List[X]) or functions (Function[A,B]), it is a bit more complicated. The only way to go is to define the subtyping rule for T[X] in terms of the subtyping rule for X but which rule do we use? - T[A] <: T[B] iff A <: B ? (covariance) - T[A] <: T[B] iff A :> B ? (contravariance) - T[A] <: T[B] iff A = B ? (invariance) Well, it depends on the type! For example, function types (A->B) are contravariant with respect to the input type (the As) and covariant with respect to the output types (the Bs). For collections it depends on what operations are allowed. Read-only collections are covariant, write-only collections are contravariant and read-write collections are invariant. This last part is where knowing about variance becomes important for programmers. When it comes to user-defined parameterized types, the variance rules are different so to find out if a given type is covariant, contravariant or invariant the only option is to read the type annotations and documentation. And you also need to know what variance is to understand those annotations when you come across them.