Category theory for computing science

What Hacker News says

1. chasMar 2021
   Programmer warning: this is the math jargon heavy version, you don't need to know the math jargon to make use of these tools for writing day-to-day programs.

   There are too many applications for me to do justice in one message and it is a bit messy because all of these are related, but there are roughly three ways that category theory gets applied to computing:

   - Reasoning about data within computer programs. In "Generating Compiler Optimizations from Proofs" they make a category where the objects are a representation of expressions in programming languages and the morphisms are expression substitutions. They use this to build general proofs of correctness of compiler optimizations (http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen...)

   - Looking at logics (and thus programming languages) as algebraic objects. Objects are propositions, morphisms are proofs that prove one proposition given assumed propositions. Similarly objects are types, morphisms are functions. That in some contexts these are the same thing is the famous (in programming language circles) Curry-Howard-Lambek correspondence. https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... For way more, see https://ncatlab.org/nlab/show/relation+between+type+theory+a... A different version of this is specifying the mathematical meaning of program execution in terms of directed-complete partial orders which are fruitful to think of categorically. I think Category Theory for Computing Science is the most approachable starting place for that perspective (https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf)

   - As core abstractions for programming. While you can reason about programs and programming languages with categorical tools, you can also use algebraic abstractions within programs. Functors, strong lax monoidal functors (called Applicative Functors in this context), and monads feature prominently in Haskell's standard library. Basic overview is here (https://wiki.haskell.org/Typeclassopedia). The default ones that Haskell uses are all defined as endofunctors on Hask (category of Haskell types and functions between them), so they look a bit funky to a mathematician, but there are other libraries with more mathematically-legible categorical tools as well. (Elsewhere in the thread, Iceland_jack linked to a discussion of one of his proposals: https://www.reddit.com/r/haskell/comments/eoo16m/base_catego...) It is also useful to describe data structures as initial F-algebras in order to abstract over the fold/reduce operation (https://blog.sumtypeofway.com/posts/introduction-to-recursio...). There is a ton more on The Comonad.Reader (http://comonad.com/reader/). For an extremely practical application of non-trivial categorical abstractions see: https://kowainik.github.io/posts/2018-09-25-co-log While I am heavy on the Haskell here because that's what I know best, people also use these abstractions in Ocaml, Scala, and other languages with enough functional and type-level infrastructure for them to be ergonomic to explicitly identify and abstract over.

   Joseph Goguen also did a ton work applying category theory to computation that spans several of the above application types. A Categorical Manifesto is probably a good place to start and he cites a ton of papers in it that are good next steps. (https://cs.fit.edu/~wds/classes/cdc/Readings/CategoricalMani...)

   Show morethread
2. escherplexOct 2018
   I'd add to that a complementary text by Barr and Wells:

   Category Theory for Computing Science (Revised 2013)

   http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf

   thread
3. arniaNov 2015
   If people are interested in reading more about how category theory can be used to help define the structure of software, there are two excellent books I can recommend.

   The first, 'Computational Category Theory' by Rydeheard and Burstall, builds a library (in Standard ML) that allows one to construct objects that satisfy properties you care about (defined in category theory terms). For example, you could define a rules system in a fuzzy logic and have the right code be automatically generated using the library.

   The second is less concrete, but probably more eyeopening. 'Category Theory for Computing Science' by Barr and Wells starts from the basic axioms of a category and ends with defining all sorts of interesting patterns for software modularity based on diagrammatic reasoning (a common tool in category theory for proving properties through simple pictures). The ideas here have helped me simplify and think more clearly about code I've been writing (in languages like Java, Python, and Ruby), even if the code isn't (ostensibly) categorical.

   Show morethread
4. nhamannJul 2013
   It first clicked for me when reading Barr and Wells' Category Theory for Computing Science [0], but I don't know about your mathematical background. Category theory is algebra, so it's probably advisable to study basic group theory before tackling category theory. (I have a hard time seeing how functors make sense until you've understood the general concept of a homomorphism, which is perhaps easiest to do in the context of groups).

   [0]: http://www.case.edu/artsci/math/wells/pub/ctcs.html

   Show morethread
5. nwhiteheadJul 2013
   Try the free online textbook Category Theory for Computing Science by Michael Barr and Charles Wells [1]. It's a true textbook with exercises and lots of content.

   [1]: http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf

   thread
6. TweyOct 2025
   Category theory is actually a ‘simplified’ graph theory, i.e. you can see categories as a restricted class of graphs. E.G. ‘Category Theory for Computing Science’ introduces categories this way (a category is a directed graph with associative composition and identity; the free category on a graph is the graph with all identities and compositions filled in). But the restrictions (associative composition and identity) are harmless and natural for programming applications where there's always a notion of ‘do nothing’ or ‘do one thing after another’, and unlock a lot of higher structure.
   Show morethread