Resources for learning practical category theory

Question

I've been doing functional programming, primarily in OCaml, for a couple years now, and have recently ventured into the land of monads. I'm able to work them now, and understand how to use them, but I'm interested in understanding more about their mathematical foundations. These foundations are usually presented as coming from category theory. So we get explanations such as the following:

A monad is a monoid in the category of endofunctors.

Now, my goal (partially) is to understand what that means. Can anyone suggest a gentle introduction to category theory, particularly one aimed at programmers already familiar with a functional language such as ML or Haskell, with references for further reading? Resources not necessarily aimed at programmers but accessible to readers with a background in discrete math and first-order logic would be quite acceptable as well.

StackOverflow thread: http://stackoverflow.com/questions/1224491/resources-for-learning-category-theory/ — sdcvvc, Dec 01 '09 at 23:07

score 46 · Accepted Answer · edited Feb 20 '21 at 15:20

Online resources:

The Catsters channel
MATH198 course notes - examples in Haskell
Rydehard, Burstall: Computional Category Theory - examples in ML (free reprint of a book)
MAGIC course
Barr, Wells: Category theory for computing science (TAC TR22 is a free reprint of the book)
Jaap van Oosten: basic category theory
Tom Leinster
Eugenia Cheng
Steve Awodey - very similar to the book mentioned by Quadrescence
Daniele Turi
Thomas Streicher
Abstract and concrete categories: the joy of cats - might be considered too verbose, but it's full of examples; slightly newer (?) version as TAC TR17
Spivak: Category Theory for Scientists - free textbook of a 2013 MIT OpenCourseWare; an updated (and non-free) version was published by MIT Press in 2014.
Emily Riehl: Category Theory in Context

Books (not free):

Benjamin Pierce: Basic category theory for computer scientists, MIT Press 1991; a slight expansion/update of the earlier (and free) CMU-CS-88-203 report
MacLane - solid mathematical foundations, but hardly any references to computing
Martin Brandenburg - Einführung in die Kategorientheorie (in german)

Category theory in Haskell:

Wikibooks introductory text
sigfpe's blog has a lot of category theory articles - (di)natural transformations, monads, Yoneda lemma...
Comonad.Reader
The Monad.Reader - check "Calculating monads with category theory"
Bartosz Milewski - Category Theory for Programmers

Another list

I can recommend, strongly, the Barr/Wells above for application connection, and the Awodey book for the theory.
And I'm glad to see my lecture notes listed! :-D — Mikael Vejdemo-Johansson, Oct 22 '09 at 22:56
@MikaelVejdemo-Johansson which ones are your lecture notes? I'm not seeing them. — Steven Shaw, Jun 04 '15 at 11:11
Some of the links here are now broken. If anybody wants to take a crack at updating them, I think that would be a valuable service to the community. — Tim Campion, Feb 20 '21 at 16:39

Justin Hilburn · Answer 2 · 2011-01-06T18:05:20.977

Since sdvccv already pointed out a number of good sources for learning category theory as applied to CS, I will try and provide some guide posts.

My favorite book on the subject is Practical Foundations of Mathematics by Paul Taylor since he does a really good job of giving you a big picture (unfortunately he doesn't always give you enough details if you don't already have a logic background). Bart Jacobs book Categorical Logic and Type Theory is also very readable.

In general I think the most important thing to understand in order to apply categories to computer science is the Curry-Howard-Lambek correspondence which loosely states that lambda calculii, intuitionist logics, and cartesian closed categories (categories where you have products and function spaces) are the same thing. Proofs and Types which was transcribed from some of Girard's lecture notes is an excellent source for the Curry-Howard part of the correspondence. Steve Awodey's book and these notes by Samson Abramsky are good places to see this translated into categorical language. For connections to Topoi Mac Lane's Sheaves in Geometry and Logic looks good.

Next you will probably want to learn about categorical and universal algebra. One of the more immediate and accessible applications of these ideas is the theory of algebraic data types (categorically: initial algebras for polynomial functors) and maps and folds between them. Monads are also a part of this subject since they are type constructors (endofunctors) that also have a multiplication and unit. Haskell do notation corresponds to forming the Kliesli category for a monad.

The nascent field of universal coalgebra has been very useful for formalizing notions of state and observation. There are also some emerging connections between coalgebra and modal logic.

Finally, if you aren't worn out you may want to learn about Stone duality which is a way of relating "logics of observable properties" and topology. For computer scientist Stone duality is primarily useful for giving a logical interpretation to domain theory, but mathematicians may recognize the duality between commutative rings and Zariski spectra as a special case.

Very good references. I think you can post using hyperlinks now. — sdcvvc, Oct 23 '09 at 14:09
Gah! Why can't I add references to this without bumping things to the first page! — Justin Hilburn, Jan 06 '11 at 18:14
I'm glad you like my (own) book, but Proofs and Types was more than "transcribed": I tried to turn Girard's weird French into natural English and Yves did a very good job of standardising the notation throughout. — Paul Taylor, Feb 22 '21 at 16:30

score 6 · Answer 3 · answered Oct 17 '09 at 18:13

6

Category Theory by Steve Awodey from Carnegie Mellon University has been a favorite text of mine. It's 266 pages, and while it's not a "practical theory book" (e.g., one aimed at programmers), it is very easy to follow and very well explained.

answered Oct 17 '09 at 18:13

Quadrescence

825

score 5 · Answer 4 · answered Oct 17 '09 at 18:25

5

TWF Week 89 for your specific question, and This Week's Finds in Mathematical Physics in general for wonderful presentations of all sorts of things category-related.

answered Oct 17 '09 at 18:25

Reid Barton

24,898

score 5 · Answer 5 · answered Oct 17 '09 at 21:00

5

Categories for the working mathematician, by Maclane, is probably good for some working computer scientists too. No disputing taste, of course.

answered Oct 17 '09 at 21:00

Scott Morrison

7,540

1

Somebody, I think it was David Rydeheard, described Mac Lane's book as the best programming manual he had ever used. – Paul Taylor Feb 12 '15 at 17:42

score 4 · Answer 6 · answered Nov 15 '14 at 13:37

To get you involved with the details of categorical computations, I've written a Web-based program that calculates products, equalisers and other constructs in the category of sets. You choose which construct you want an example of, then fill in values for some of its objects and arrows, and my program will compute the remaining ones, then send back a drawing of the diagram with values for all objects and arrows, plus an explanation.

score 3 · Answer 7 · answered Oct 26 '09 at 15:32

You may find Computational Category Theory by Rydeheard and Burstall interesting. It's available online at Rydeheard's page: http://www.cs.manchester.ac.uk/~david/categories/

The Manual there is the textbook and The Programs provide a great deal of the ML code in the text in its development of category theory.

For someone new to CT it's very different than most introductions but the code helps make some of the ideas much more concrete.

score 3 · Answer 8 · answered Oct 17 '09 at 18:22

3

The book "Abelian Categories, an Introduction to the Theory of Functors" by Peter J. Freyd is a very good introduction to category theory. It is not aimed at computer scientists, but it is a good introduction to the subject.

answered Oct 17 '09 at 18:22

GMRA

2,050

score 3 · Answer 9 · answered Oct 17 '09 at 19:43

3

I'm skeptical of "practical category theory," especially books by mathematicians telling computer scientists how important category theory is. I'm not saying there aren't connections -- I know there are -- but there's a tremendous temptation for mathematicians to include gratuitous material.

answered Oct 17 '09 at 19:43

John D. Cook

5,147

3

The Barr/Wells book is not very heavy on the gratuitious material - it puts quite some energy into the Sketch theory formalism (Wells' big thing), but otherwise does a good job of relating almost everything to various corners of computer science. – Mikael Vejdemo-Johansson Oct 22 '09 at 23:00

score 1 · Answer 10 · answered Mar 16 '18 at 18:45

I enjoyed Categories and Computer Science by RFC Walters, and it is the one book that got me anywhere toward understanding what categories might be good for:

https://www.amazon.com/Categories-Computer-Science-Cambridge-Texts/dp/0521422264/ref=sr_1_7?ie=UTF8&qid=1521225555&sr=8-7&keywords=category+theory+computing+science

Ivan Di Liberti · Answer 11 · 2018-03-16T23:29:40.967

1

There is also a book from Pedicchio and Tholen: Categorical Foundations.

If you are interested in categorical logic, I recommend to give a look to History of categorical logic, by Reyes and Marquis.

Probably a good place to start for a computer scientist might be the book from Adamek and Trnkova: Automata and Algebras in Categories.

edited Mar 16 '18 at 23:29

answered Mar 16 '18 at 18:55

Ivan Di Liberti

8,176

Resources for learning practical category theory

11 Answers11

Linked