[Solved]: Reference request: Category theory as it applies to type systems

Problem Detail: 

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.

Asked By : gardenhead

Answered By : Martin Berger

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.

• Categories for Types by Roy Crole
• Introduction to higher order categorical logic by Joachim Lambek and Phil Scott.

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/63990