Covariance, Contravariance and Order Theory
In this post I make the observation that covariance and contravariance in programming are what are known as Order Duals. I am not the first person to make this observation, however, these ideas often tend to be buried in academic research papers like "Adding Axioms to Cardelli-Wegner Subtyping" by Anthony J H Simons, don’t get me wrong I love these types of papers, they give me hope and inspiration that software engineering will someday become a first class engineering citizen. Unfortunately, these types of papers tend to be too theoretical and thus not very accessible for the average developer. This is unfortunate as the idea of covariance and contravariance as order duals both puts these concepts into the mathematical context of order theory and possibly gives programmers some native context for order theory. So hopefully this post will make these ideas more programmer friendly.
I previously wrote a post about lattice theory, which is part of the more general order theory, where I talked about some basic order theory ideas such as duality. Order theory occurs quite a lot in software and programming and this is part of a series of posts to talk about those occurrences.
Covariance and contravariance receive a fair amount of attention, as they should, in software blogs and some of these posts include some interesting observations. One, perhaps slightly off topic observation, is "Liskov Substitution Principle is Contravariance" which is an interesting observation and interesting post if you overlook the disdainful tone towards OO. Another more relevant post which is a nice post about "Covariance and Contravaiance in Scala" relates these ideas to category theory which is relevant especially since apparently you can think of "Category Theory as Coherently Constructive Lattice Theory", warning heavy going in that paper.
Defining Covariance and Contravariance
To me one of the most striking and perhaps apropos examples of order theory in software is that of covariance and contravariance which Eric Lippert defines on his blog as:
The first thing to understand is that for any two types T and U, exactly one of the following statements is true:
- T is bigger than U.
- T is smaller than U.
- T is equal to U.
- T is not related to U.
For example, consider a type hierarchy consisting of Animal, Mammal, Reptile, Giraffe, Tiger, Snake and Turtle, with the obvious relationships. (Mammal is a subclass of Animal, etc.) Mammal is a bigger type than Giraffe and smaller than Animal, and obviously equal to Mammal. But Mammal is neither bigger than, smaller than, nor equal to Reptile, it’s just different.
He has an eleven part series on covariance and contravariance, his posts cover some C# implantation details but the ideas are generally applicable and looking at one language’s details can help with comparing and contrasting to other languages.
Wikipedia includes the following definition, the animal example is pretty popular:
- Covariant: converting from wider (Animals) to narrower (Cats).
- Contravariant: converting from narrower (Triangles) to wider (Shapes).
- Invariant: Not able to convert.
Including this is slightly redundant but this definition captures the conversion aspect and defines the relationships explicitly.
Covariance and Contravariance as Order Duals
The above are definitions that have order theory written all over them. In fact that is pretty much a text book definition of an order Relation in that it is reflexive, transitive, and antisymmetric. It is reflexive since Animal = Animal, transitive since Animal ≤ Mammal ≤ Cat implies Animal ≤ Cat, and antisymmetric since Animal ≤ Mammal implies not Animal ≥ Mammal and in the animal example there are cases of both comparability and incomparability as you would find in a partial order.
As you can see from the above definitions both sets of terms, wider/narrower or bigger/smaller, which are the same, define an order dual for comparison. To write it more formally we will call the set C classes of various types in an OO hierarchy. So covariant would be represented by less than or equals ≤ and contravariant would be represented by greater than or equals ≥ and a set of classes with these order relations can be written with mathematical notation as (C, ≤) = (C, ≥)d .
Types as Sets of Fields
It was in researching this post that I came across the paper "Adding Axioms to Cardelli-Wegner Subtyping". These kinds of discoveries are one of the reasons I write these posts. In that paper they quote another paper "On understanding types, data abstraction and polymorphism" by Luca Cardelli and Peter Wegner:
a type A is included in, or is a subtype of another type B when all the values of type A are also values of B, that is, exactly when A, considered as a set of values, is a subset of B
The ideas about types and subtypes covered in these papers extend beyond which fields a class or object has, however, I thought it would be interesting and beneficial to limit the discussion to that case. One reason is that if you take the fields of an object or class then all subtype collections of fields will be found in the powerset and all subtypes will be a subset relation and these can be drawn as my favorite lattice, yes I have favorite lattice, the powerset lattice. Also in this case covariance and contravariance are now defined as the subset and superset operations on the powerset lattice.
Types as Sets of Fields in the Real World
Now I always feel that a real example helps quite a bit so I have created a set of example classes, Scala traits actually, which illustrate the above ideas using a quasi-real-world example. Please note that these code examples are designed for the purposes of illustrating these ideas and may contain design issues that one would not implement in the real world, but they should be close enough to bridge the conceptual gap, if you will. Also this first example is should be applicable to dynamically typed languages that might use duck typing or structural typing.
The following Scala traits define a possible domain object hierarchy that could be used to persist data to a database and render it back to a web page among other possible uses:
trait BaseDomain {
override def equals(that: Any) : Boolean
override def hashCode : Int
}
trait PersonInfo extends BaseDomain {
var firstName : String
var lastName : String
}
trait Address extends BaseDomain {
var street : String
var street2 : String
var city : String
var state : String
var country : String
var zipCode : String
}
trait PhoneNumber extends BaseDomain {
var phoneNumber : String
var extension : String
}
trait Person extends BaseDomain {
var personInfo : PersonInfo
var address : Address
var phoneNumber : PhoneNumber
}
These traits yield the following field powerset lattice:
Now suppose we would want to define a type for each of the above lattice points, which we probably would not do but there may be cases to do similar types of things in the real world. Let’s define the following Scala traits that wrap the above domain object hierarchy elements:
trait PersonInfoTrait extends BaseDomain {
var personInfo : PersonInfo
}
trait AddressTrait {
var address : Address
}
trait PhoneNumberTrait extends BaseDomain {
var phoneNumber : PhoneNumber
}
trait PersonInfoAddressTrait extends AddressTrait with PersonInfoTrait {
}
trait AddressPhoneNumberTrait extends AddressTrait with PhoneNumberTrait {
}
trait PersonInfoPhoneNumberTrait extends PhoneNumberTrait with PersonInfoTrait {
}
trait PersonTrait extends PersonInfoAddressTrait with AddressPhoneNumberTrait with PersonInfoPhoneNumberTrait {
}
Since Scala traits support multiple inheritance we can define the above type hierarchy which can be drawn as the powerset lattice that it is:
Again we can see covariant and contravariant types defined on this lattice and each relation is actually the subset superset relation on fields.
I feel the basic observations and the above examples on order duals and covariance and contravariance make the ideas pretty strait forward for field set context. In writing this I delved into a number of papers, adding some of them to my "to read list", on Types in programming and Type Theory and I feel there are probably some deeper insights and implications of all this.
