Teaching Category Theory to Computer Scientists

Category theory has long served as a deep mathematical theory for investigations in programming languages and semantics. Though its influence and popularity have varied over time, recent years have seen renewed interest in applying category theory to computer science: for instance, in type theory, automata, quantum computing, and many other areas.

This past fall, I redesigned a graduate class called “Category Theory for Computer Scientists”. Though I admittedly do not consider myself to be an expert in category theory, I think the design of this kind of class is underexplored and there is room for experimentation. Here, I’d like to describe my experience teaching category theory to computer scientists and what I learned. If you’re impatient to see the details, the final materials are on the course’s website.

Even if you’re not so interested in category theory, as computer science becomes an increasingly mathematical field, we are often faced with a question: should we teach a mathematical topic “for computer scientists”, or should we refer students to an existing course in the math department? There are pros and cons to both approaches, and I’ll return to these broader questions at the end.

What’s So Hard about Teaching Category Theory?

There are two main difficulties in designing a course about category theory.

High level of abstraction. Category theory works at an extremely high level of generality, layering abstraction on top of abstraction. Examples are crucial to keep the material grounded, but finding good examples is difficult. Category theory can be applied to many different fields, and interesting examples often require knowledge about some other application area. The common teaching approach is to illustrate ideas using small examples from set theory and algebra as a kind of least common denominator. However, it is difficult to show more substantive examples without assuming more domain knowledge, and I think a course targeted towards computer scientists should draw examples from CS.

Breadth of the topic. Category theory is sprawling. The central concepts are all interrelated, and it is difficult to form the material into a linear narrative. While there is a central core that all courses cover, beyond there is a bewildering array of concepts and it is not obvious which parts should be covered; worse, application areas often rely on completely different sets of tools. The common teaching approach goes through a list of topics one after the other, but the result can feel a bit like a laundry list.

Course Design

To address these difficulties, we can look to how category theory is taught in mathematics. Somewhat ironically, category theory is typically not a standalone course in math departments. Instead, students learn category theory while studying another area of math, typically algebra or topology. Indeed, category theory was originally developed to solve problems in algebraic topology.

Inspired by this approach, our category theory course focused on applications in programming language semantics. By centering this area, we could illustrate specific category theory concepts through more interesting examples. We could also used the application domain to organize the course: proceeding from simpler languages to more complex languages, and interleaving lectures on category theory with lectures on semantics for different languages.

Materials and Organization

To implement this course, we drew on a range of materials. For first half, we followed Categories for Types (CfT) by Roy Crole. This is a somewhat unusual choice for a course on category theory, but it was ideal for our design: it presents categorical semantics for a sequence of programming languages, illustrating how tools from category theory can be used to model specific language features. Besides showing how to define semantics for languages, each chapter ends with a substantial application. The book is self-contained and shows explicit detail of almost all calculations, something which might be tedious for experts but which is useful for students learning the material for the first time.

In the second half, we drew from classic papers and notes on other topics in programming languages. The general focus was not the specific results in the papers; rather, our goal was to use each paper to illustrate some specific concepts in category theory. We also supplemented with a more traditional textbook on category theory, such as Leinster. CfT introduces all of the category theory that it needs, but the presentation is quite terse and rather dense.

The resulting course was organized by application topic, with each section also covering some relevant aspects of basic category theory. Algebraic theories served as natural bookends, first as an example of a basic programming language, and finally in connection with algebraic effects. The outline looked something like this:

• Algebraic Theories (first-order languages)
  • CT: categories, functors, natural transformations, products
  • Application: syntactic category, Lawvere’s functorial semantics
• Simply-Typed Lambda Calculus (STLC)
  • CT: Cartesian Closed Categories, Yoneda Lemma, representable functors
  • Application: semantics of STLC, categorical gluing, conservativity
• System F
  • CT: adjunctions, indexed categories
  • Application: semantics of System F
• Inductive and recursive types
  • CT: limits and colimits, fixed points of functors
  • Application: semantics of inductive types, domain equations
• Linear types
  • CT: symmetric monoidal categories, touch on comonads
  • Application: linear/non-linear model of linear logic
• Effects
  • CT: monads, algebras, Kleisli category
  • Application: monads for effects, algebraic effects and handlers

Lessons Learned

I had a great time teaching the course to a mixed audience of around 25 students, mainly from computer science students but also some from mathematics. Initially the course was more graduate heavy, but by the end it surprisingly skewed undergraduate. After discussing with students and reflecting, I think this course design has some strengths and weaknesses.

Strengths. Students strongly enjoyed learning about category theory interleaved with material on programming language semantics. They felt that the examples and more in-depth applications gave them a better sense of what category theory could be used for, at least in this particular domain. Breaking up the pure category theory material also helped make the course less monotonous.

Weaknesses. The biggest weakness students pointed out is that they didn’t get much motivation for categorical semantics. This was partially my fault, but given time constraints, it seems hard to expect this course to also function as a full course on denotational semantics. Indeed, I consciously dropped many topics (e.g., domain theory) which would have been nice to cover, but would have taken too much time to do properly.

Students also said that though they were impressed by the applications, they still didn’t get a sense of how to apply category theory in their own work. This is also a fair criticism, but one I’m not sure how to address—perhaps this course can only serve as a starting point, and students simply need more experience before they can become category theory practitioners. Or, for students that have more background in programming languages, maybe it would be useful to show how to recast proofs using operational semantics into categorical language.

Finally, I was worried that with this course design, students wouldn’t get enough experience with doing complex proofs and calculations; while these aspects are not so fun and tedious to show in class, they are indispensable for using category theory, as opposed to just reading about it. Students were mixed on this point—they all agreed that they didn’t want to use class time going through calculations, but they would have appreciated more exercises where they could develop this skill.

Broader Questions: Teaching X for Computer Scientists?

While category theory is not a topic that most computer science students will come across, many areas in computer science are relying on more mathematical tools. There are no easy answers about whether we should expect computer science students to learn these topics in math courses, or whether we should design versions of these topics tailored for computer science. Looking back, I think there are three reasons why computer science is a natural home for a category theory course.

First, most mathematics departments do not have a standalone category theory course. While students with a computer science background could learn this material through other math courses, taking a homological algebra course seems too far off the main path to recommend to computer science students.

Second, there are natural areas of computer science—for instance, programming language semantics—where we can illustrate most concepts of basic category theory. Having a specific application area allows going deeper on examples, and also makes the course feel more cohesive.

Finally, there is plenty of interest in computer science students to learn category theory. This interest is not to be underestimated—I was constantly surprised at how students in our class persevered through difficult material and hairy calculations, and I was doubly surprised at how many undergrads were passionate about the topic.

Final Thoughts

In this post I’ve described one route for teaching category theory to computer scientists, but I believe there are many other possible approaches. For instance, our course was purely theoretical—could it make sense to approach this material from a more computational perspective, perhaps implementing constructions from category theory? I hope to continue experimenting in the future, and if you’re also looking to teach this kind of course, don’t hesitate to reach out!

Acknowledgments: This new course would not have been possible without a great group of students at Cornell, and dedicated teaching assistants. Pedro Azevedo de Amorim and Keri D’Angelo played a huge role in developing the course materials. Arthur Azevedo de Amorim, Carlo Angiuli, Max New, and Jon Sterling provided useful feedback on the course materials, from the perspective of researchers in category theory; Carlo also suggested the picture. Finally, Adrian Sampson greatly improved this post with numerous edits and suggestions.

Bio: Justin Hsu is an Assistant Professor of Computer Science at Cornell University. Despite teaching a course about category theory, he still doesn’t think he understands it very well and hopes to learn and teach it more in the future.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.