Stuff about programming
Remembering when to use covariant and contravariant types.
Bookmark and Share

Covariant and contravariant types creep up in the subtyping rules for functions, I/O channels (such as in the Pi-calculus) and with generic collections such as lists.

The general rule is approximately that writes are contravariant and reads are covariant.

Let's write A <: A' to means that A is a subtype of A'. In class-based object oriented languages, the subtype relation is induced by the class hierarchy. Generally, a type T is covariant within its constructor C when T <: T' implies C[T] <: C[T']. That is, the direction between T and T' is preserved. The type is contravariant when T <: T' implies C[T'] <: C[T]. That is, the direction between T and T' has been flipped around in the other direction.

When thinking about types, I find it useful to remember the subsumption rule. If we have that A <: A' and x has type A (x:A), we also have that x has type A' (x:A'). The subtype relation <: is reflexive (A <: A) and transitive (A <: B and B <:C implies A <: C). This subsumption rule is formally written:

x: A A <: A' x: A'

Function types.

In terms of functions, parameter types are contravariant and return types are covariant. The subtyping rule for a function type is:

A' <: A B <: B' A -> B <: A' -> B'

Using the subsumption rule we have that if f: A -> B and A' <: A and B <: B' then f: A' -> B'

Intuitively, this rule ensures that it is safe to pass to f more information (a narrower type) in its argument and to take less information (a wider type) from its return value. The converse of this rule would be unsafe.

Java 1.5 introduced covariant return types for class methods, which can be understood in terms of function subtyping.

When a Java class C has a method m: A -> B then a class C' with C' <: C can override m with m: A -> B' where B' <: B. By the subtyping rule for functions, we have that A -> B' <: A -> B. Thus when o: C and o':C' then the assignment o = o' is safe as the invocation o.m(a) will return a value that is a subtype of B.

Communication channels in the Pi-calculus.

Communication channels in the pi-calculus are typed with input and output capabilities. The chanel types are output T, input T and #T. The output type is contravariant, the input channel is covariant and the input/output chanel, #T, is invariant.

Intuitively, this means that if a channel is contractually agreed to send values of type T then it is type-safe for a sender to output more information on the channel (to send values of type T' contravariantly such that T' <: T). If a chanel is contractually agreed to receive values of type T then it is type-safe for a receiver to input less information from the channel (to read values of type T' covariantly such that T <: T').

The subtyping rules for input and ouput channels show that the output chanel is contravariant, with the direction between T and T' flipped around in the opposite direction:

T <: T' input T <: input T'

T' <: T output T <: output T'

Generics.

The put-get principle for generic collections states that it is safe to use a generic collection of values of type T contravariantly for putting/writing/storing and covariantly for getting/reading/retrieving.

Java's syntax for covariant generic types is C<? extends T> and its syntax for contravariant generic types is C<? super T>.

We could try to make sense of generics by writing the subtyping rules for Java's generic wildcard types like this:

T <: T' C<T> <: C<? extends T'>

T' <: T C<T> <: C<? super T'>

while remembering the subsumption rule, we have that a collection of type C<T> can be typed either contravariantly for writes or covariantly for reads.

The subtype relation is naturally defined between wildcards:

T <: T' C<? extends T> <: C<? extends T'>

T <: T' C<? super T'> <: C<? super T>

Java's type system seems to enforce type-safety by using two extra rules, one for parameters and one for return values. That is, when a type variable E is instantiated with ? extends T and E e is a parameter of a method then every value is untypeable as an argument(kind of like a bottom type, perhaps). When a type variable E is instantiated with ? super T and E is a return value of a method then every value returned is typed to Object, which is the root of the class hierarchy (like a top type).

Thus, generic covariant types are useful as return values of methods and generic contravariant types are useful as parameters to methods.

blog comments powered by Disqus
Website created by Nicholas Nguyen.