How Type Variance fits into Category Theory

Category theory

Before jumping into the what is a “category”, we are going to review some examples that lead to its definition.

Sets

The first example is sets (in the mathematical sense, i.e., something that contains “elements”) and functions. When you have two sets A and B, you can have functions between these two sets, from A to B, written f: A -> B. A function is simply a “machine” that takes all elements in A (the domain) and maps them to an element in B (the co-domain). For example, A could be the set of all objects in a store, B the set of (positive) real numbers, and f would associate its price to each object in A.

(f◦g)◦h = f◦(g◦h)

Groups

Sets are not that exiting, because there is nearly no structure in them. Between two sets, you have plenty of functions because “everything” is basically allowed. Things become quickly much more interesting when we add a little bit of contraints (aka, structure). A group is a set with additional properties. It has an internal binary operator °, such that for two elements a and b, you can create another element a ° b. It also has a special element e, called the neutral element, and every element has an “inverse”.

Monoids

A very similar example can be found in monoids. Monoids are like groups, except that it is not required that elements have an inverse.

Others

There are plenty of other examples of mathematical structures that have similarities with groups and monoids. Among them, there are, for example, vector spaces, fields, algebras, topological spaces… Don’t worry if you don’t know any of these terms! They’re just a short list to demonstrate that categories really didn’t come out of nowhere.

Category

With these three examples, we are ready for the definition of a category. The common important point in these examples is that there are stuff (sets, groups, monoids) that may be linked together (respectively with functions, morphisms of groups and monoids). Moreover, these links can be composed together. This is basically all the ideas encapsulated in the definition.

Is there a category of categories?

It is when you ask this kind of questions that you start to understand why some mathematicians end up mad. Yet, the answer will prove extremely relevant in our case. A “category of categories” would be a category where the objects are categories. But what are the arrows? They’re called “functors”, and here is what they do.

Objects are not containers!

In all the common examples of categories, the objects are sets, or at least “containers” of stuff. It is absolutely not required. Even, it is against the philosophy of category theory to consider objects as sets. An example of a category where the objects are not “containers” is the category where objects are natural numbers, and you define that there exists an arrow f: n -> m if, and only if, m is divisible by n. That is, m is 0 modulo n.

Is there a category of functors?

Well yes, but that is going a little bit too far for us today…

Type Variance

Type variance describes how type inheritance transforms itself in type parameters. Depending on how much you understand this sentence, you can freely skip this section. If not, we are gonna decompose it together.

  • yes, a list of horses is a list of animals
  • no, a list of horses is completely different from a list of animals
  • no, actually a list of animals is a list of horses.

How type variance fits into category theory

Finally, we arrive at the core of this post, namely the link between type variance and category theory. If you’ve read it through, you can guess that the link stands in the “covariant” and “contravariant” terminologies. We’re going to define a category, and functors from that category to itself, to make the link with type variance.

  • a covariant functor if T is covariant as a type parameter (we will write F[+T])
  • a contravariant functor if T is contravariant as a type parameter (we will write F[-T])
  • no functor (sadly) if T is invariant (we simply write F[T]).
Function[Function[T, Boolean], T]

Conclusion

In this post, we discovered the definition of categories, alongside several examples, we discussed a little bit the topic of type variance, and we linked the two of them in a nice way.

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store