I keep hearing about how one must learn category theory to truly understand programming language theory. So far, I've learned a good deal of PL without ever stepping foot into the realm of categories. However, I figured it was time to take the leap to see what I had been missing.

Unfortunately, none of the sources I can find seem to make any connections to type systems or programming. They say it's an introduction to category theory for computer scientists, but then veer off into general abstract nonsense (I say this lovingly) without giving any practical examples or applications.

I guess my question is actually two-fold:

  1. Is category theory essential for understanding the "deep concepts" in PL?
  2. What's a source that explains category theory from the viewpoint of practical applications to type systems and programming?

So far, the furthest I've gotten is to a vague conception of functors (which don't seem to be related to functors in ML, as far as I can tell). I'm dreading the abstraction I'll need to keep in my head to understand monads from a category-theoretic view.

  • 2
    $\begingroup$ @Raphael It is a bad idea to ask a question which consists of two different questions only vaguely related to each other. But question 1. is not subjective. It is rather a request for clarification and explanation. I guess question 2. was meant in the sense that he is happy with a reference to a place where it is explained instead of an actual explanation too. $\endgroup$ – Thomas Klimpel Sep 28 '16 at 7:57
  • 2
    $\begingroup$ In the future, it's better to ask just one question per post. You can ask question 1, then depending on the answers you get, decide whether to ask question 2 separately. That often makes things go more smoothly. $\endgroup$ – D.W. Sep 28 '16 at 17:20
  • 1
    $\begingroup$ @Raphael How is question one subjective? It might be hard to judge – is that what you mean? And it might have as an answer “It depends on which kind of person you are.” – is that what you mean? It still might turn out that it is definitely essential or definitely not essential, right? (And people seem to agree that it is not essential.) $\endgroup$ – k.stm Sep 28 '16 at 19:15
  • 1
    $\begingroup$ @k.stm The general shape of the question worries me. If somebody were to ask, "Is algebra essential to understanding the deep concepts of formal languages?", I know for a fact that different people will give different answers -- based on their preferences and taste. I don't expect it to be different here. $\endgroup$ – Raphael Sep 28 '16 at 22:16
  • 1
    $\begingroup$ @Raphael Okay, I get it. But I think that’s people giving subjective answers to an objective question. (Feels like people saying “Oh, I’m drinking five cups a day and I feel great!” when asked whether coffee is healthy or not.) $\endgroup$ – k.stm Sep 29 '16 at 7:20

Category theory is not necessary to understand programming languages, it's not even necessary to do advanced research on programming languages. Most programming language people don't know (much) category theory.

Category theoretical methods have been useful mostly in a small part of programming language research, namely in the analysis of functional programming, particularly, since Moggi's great discovery that some computational effects have monadic structure. In the 1990s, following Moggi's breakthrough, a lot research was done to extend categorical methods to other forms of programming languages. However, to the best of my knowledge categorical methods have not been found all that useful for OO, concurrent, parallel and distributed computation, timed computation or compilers. For this reason, people have mostly abandoned extending categorical methods.

Categorical approaches to typed programming work well in pure functions. Indeed some simple typing systems are categories. This is described in e.g.

There is now a lot of work on types for concurrent processes (e.g. session types) and none of that is categorical in nature as of Sept 2016.

That said, one can never know too much mathematics, and knowing category theory is useful. So it's a question of cost/benefit. If you like maths, if maybe you have a bit of background in algebra (e.g. what's the free group over a set, free ring etc) then learning category theory will be easy, and if you plan on doing work that is (inspired by) functional programming, knowing categories will be useful.

Finally, category theory is beautiful mathematics, and worth studying simply because it's so neat.

See Uday Reddy's contribution in this discussion for a different view.

  • $\begingroup$ "However, to the best of my knowledge categorical methods have not been found all that useful for..." That's exactly my issue. Operational semantics can accurately describe all these concepts, so I didn't feel like I was missing out. I love mathematics, but my background in abstract algebra is sadly lacking. I only understand the bare basics of the common algebraic structures. This has made grasping category theory especially cumbersome. $\endgroup$ – gardenhead Sep 28 '16 at 14:10
  • 2
    $\begingroup$ @gardenhead Then maybe CT isn't all that useful for you. If you want read a lot of papers in the "Functional Programming" space, including work on types, then a lot of them will use the language of CT though. $\endgroup$ – Martin Berger Sep 28 '16 at 14:50
  • $\begingroup$ Is this one a duplicate? $\endgroup$ – Raphael Sep 28 '16 at 22:16
  • 2
    $\begingroup$ I'd additionally suggest the book cs.unibo.it/~asperti/PAPERS/book.pdf "Categories, Types, and Structures", which is apparently out-of-print, but that's a link to a pdf from one of the authors' homepages, so I guess it's legit. $\endgroup$ – John Forkosh Sep 29 '16 at 10:09

Learning category theory is a huge time investment, and the question whether it is worth it is very valid. I still struggle with this too, and I already know why I should learn it. I wrote:

I liked assembly language when I started to program, and set theory feels similar to assembly language. Category theory is one alternative to get around all the engrained prejudices about logic and model theory embedded into mainstream ZFC set theory.

The idea here is to use categories instead of sets or "unspecified bits" as a possible semantics for a given type theory or programming language. Why should one want to do this? Consider the duality between an action and an observation. Different observations (or at least their order in time) don't interfere with each other (outside of quantum mechanics), but this is not necessarily true for different actions. The engrained prejudices about logic embedded in set theory make it hard to model actions, compared to modeling observations.

I'm not convinced that there really is a perfect correspondence between category theory and type theory like claimed here:

By a syntax-semantics duality one may view type theory as a formal syntactic language or calculus for category theory, and conversely one may think of category theory as providing semantics for type theory.

It is true that category theory can provide semantics for type theory (which can be really useful), but I doubt that type theory really provides a sufficiently powerful formal syntactic language to express all the calculations done in category theory.

In practice, the usefulness of category theory can arise by suggesting useful questions and analogies. But category theory can also suggest activities and questions which in the end turn out to be just a distraction (waste of time) from the really important issues. And you certainly can learn logic and type theory without caring about category theory.

  • $\begingroup$ Thanks for your thoughts. Your reasons for learning category theory seem to be different from mine; you're interests stem from a pure-mathematical perspective, while I would like to broaden my understanding of types. Still, it's nice to know that other people besdies myself find category difficult to approach and apply $\endgroup$ – gardenhead Sep 28 '16 at 14:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.