could someone explain the connection between type covariance/contravariance and category theory?

Question

I am just starting to read about category theory, and would very much appreciate it if someone could explain the connection between CS contravariance/covariance and category theory. What would some example categories be (i.e. what are their objects/morphisms?)? Thanks in advance?

Answer 1

A contravariant functor from $C$ to $D$ is the exact same thing as a normal (i.e. covariant) functor from $C$ to $D^{op}$, where $D^{op}$ is the opposite category of $D$. So it's probably best to understand opposite categories first -- then you'll automatically understand contravariant functors!

Contravariant functors don't come up all that often in CS, although I can think of two exceptions:

1. You may have heard of contravariance in the context of subtyping. Although this is technically the same term, the connection is really, really weak. In object oriented programming, the classes form a partial order; every partial order is a category with "binary hom-sets" -- given any two objects $A$ and $B$, there is exactly one morphism $A\to B$ iff $A\leq B$ (note the direction; this slightly-confusing orientation is the standard for reasons I won't explain here) and no morphisms otherwise.

   Parameterized types like, say, Scala's PartialFunction[-A,Unit] are functors from this simple category to itself... we usually focus on what they do to objects: given a class X, PartialFunction[X,Unit] is also a class. But functors preserve morphisms too; in this case if we had a subclass Dog of Animal, we would have a morphism Dog$\to$Animal, and the functor would preserve this morphism, giving us a morphism PartialFunction[Animal,Unit]$\to$PartialFunction[Dog,Unit], telling us that PartialFunction[Animal,Unit] is a subclass of PartialFunction[Dog,Unit]. If you think about that, it makes sense: suppose you have a situation where you need a function that works on Dogs. A function that works on all Animals would certainly work there!

   That said, using full-on category theory to talk about partially ordered sets is big-time overkill.

2. Less common, but actually uses the category theory: consider the category Types(Hask) whose objects are the types of the Haskell programming language and where a morphism $\tau_1\to\tau_2$ is a function of type $\tau_1$->$\tau_2$. There is also a category Judgments(Hask) whose objects are lists of typing judgments $\tau_1\vdash\tau_2$ and whose morphisms are proofs of all the judgments on one list using the judgments on the other list as hypotheses. There is a functor from Types(Hask) to Judgments(Hask) which takes a Types(Hask)-morphism $f:A\to B$ to the proof

     B |- Int
    ----------
      ......
    ----------
     A |- Int

which is a morphism $(B\vdash Int)\to(A\vdash Int)$ -- notice the change of direction. Basically what this is saying is that if you've got a function that turns A's into B'a, and an expression of type Int with a free variable x of type B, then you can wrap it with "let x = f y in ..." and arrive at an expression still of type Int but whose only free variable is of type $A$, not $B$.

Answer 2

There are very nice videos about contravariance/covariance in Going deep channel in Microsoft Channel9. You can start here:

• E2E: Brian Beckman and Erik Meijer - Co/Contravariance in Physics and Programming, 1 of 3
• E2E: Brian Beckman and Erik Meijer - Co/Contravariance in Physics and Programming, 2 of 3
• E2E: Brian Beckman and Erik Meijer - Co/Contravariance in Physics and Programming, 3 of n
• E2E: Whiteboard Jam Session with Brian Beckman and Greg Meredith - Monads and Coordinate Systems