7 ms·

I love category theory. I found out about it through Haskell and as it turns out it is a branch of mathematics that I feel I’ve been missing my whole life. Sin

I love category theory. I found out about it through Haskell and as it turns out it is a branch of mathematics that I feel I’ve been missing my whole life. Since taking an interest I’ve worked through a couple books on the topic and have listened to a ton of talks/interviews Emily Riehl has given (as well as others). I really enjoyed her talk at lambda world, “A categorical view of computational effects” (both the content and audio/video quality of this talk are very good!) Stoked to see this article on HN! I can’t tell if category theory is becoming more popular or if I’m just living in a algorithmically curated/tailored world.

jamiek88 6y ago
What was the number one thing about category theory that changed your perspective if you don’t mind me asking? You seem very enthusiastic and I’d like to share that enthusiasm one day.
- bopbeepboop 6y ago
  Not the person you’re asking, but the “aha” moment for me was connecting whiteboard diagrams with type theory. Whiteboard diagrams work because they’re a categorical diagram related to the semantics of the program I’m trying to write. In the sense that CT and TT are “equivalent”, your whiteboard diagrams are your program.
- type_enthusiast 6y ago
  For me, it was realizing that category theory is the mathematical language of abstraction – almost literally the "principle of least power" in math – and those abstractions often connect to programming abstractions. Even if you're not using words like "Functor" or "Monad" to describe them! And it can be useful to think of them more abstractly than they actually are, even if you're not going to use them that way (or even talk about them that way in your code). Just making some "ridiculously abstract" connections can help provide a missing piece of architecture, even if you keep the math story to yourself (which you likely should). So it can (potentially?) be useful to model various things in terms of what they mean "at the most abstract level", and then find ways to capture chunks of that into various architectural abstractions that make sense without category theory (kind of like a Karnaugh map, in a sense). Sorry if that seems like a lot of "purple prose" or self-important... it really isn't. I think it's the same thing that a lot of people mean when they say "I don't use Haskell but learning it made me a better programmer." I don't use abstract algebra, but learning it made me a better programmer (those statements might even be homomorphic, depending on the Haskell involved)
- chas 6y ago
  The first thing that got me really enthusiastic in category theory was seeing the definition of the categorical product in terms of universal properties. It's a very simple, but very different way of defining objects that makes it easy to see the relationships between similar objects in different contexts. For example, multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming are all products in particular categories* and the universal property definition unifies them very nicely. There isn't really enough space here to spell it out in detail, but this[0] is a good explanation. There is also a very natural way to manipulate the definition (categorical duality) to get coproducts which unify things like logical disjunction (||), greatest common divisor, and disjoint union of sets. This extremely unified view is also nice because if you have an unfamiliar mathematical or computational object, but you know that it has a categorical product, you suddenly know a ton about what you can do with it as well as some interesting questions to ask and properties to go looking for. This genre of abstraction is all over the place in category theory and it gets way more interesting, but seeing products defined like this and how incredibly unifying of an abstraction it is was the first place that I really saw what the categorical perspective brought to the table. *Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about the action on objects), least common multiple within the category of positive integers ordered by divisibility (a partial ordering being just a special kind of category), logical conjunction within the category of truth values (which can be thought of as sets with at most one element), and structs or record types in the category whose objects are the types of your favorite programming language and morphisms are the programs between them. (From Chinjut, last time I brought up categorical products on hn: https://news.ycombinator.com/item?id=8780786 https://news.ycombinator.com/item?id=8780786) [0] https://rnhmjoj.github.io/category-theory-for-programmers/src/part-1/chapter-5.html https://rnhmjoj.github.io/category-theory-for-programmers/sr... If you'd to see how this applies more directly to programming, work like this is a direct application of the same definitional strategy for abstraction: https://blog.sumtypeofway.com/posts/introduction-to-recursion-schemes.html https://blog.sumtypeofway.com/posts/introduction-to-recursio...
- adamnemecek 6y ago
  For me it was the idea of adjoint functors which is the central idea of category theory. I wrote up a bit on it here https://github.com/adamnemecek/adjoint https://github.com/adamnemecek/adjoint
mauflows 6y ago
What are your favorite books on the topic?
- KirillPanov 6y ago
  Steve Awodey's Category Theory, hands down. https://www.goodreads.com/book/show/2047855.Category_Theory https://www.goodreads.com/book/show/2047855.Category_Theory It's a mathematics book written by a philosophy professor that is extremely readable for computer scientists. Very CMU, much wow, such deduction.
tkgally 6y ago
I had a brush with category theory more than forty years ago. I got a master’s degree in math at the University of Chicago in 1980, Saunders Mac Lane was on the faculty, a few grad students were doing category theory, and I worked through part of Mac Lane’s Categories for the Working Mathematician on my own. I left mathematics soon after—with some regret—and haven’t kept up with the field. The interview with Emily Riehl and the introduction (which I read just now) to her book Category Theory in Context suggest that the field has made a lot of advances in the years since. I have a question for people who are familiar with recent developments. Forty years ago, the opinions of other math grad students about category theory were divided. Some thought it had the potential to yield great breakthroughs and solve previously unsolved problems in many branches of mathematics. Others thought it was pretty and useful for identifying similar structures in different fields but wasn’t much use for making significant new mathematical discoveries. A sentence in Emily Riehl’s book—“The category-theoretic perspective can function as a simplifying abstraction, isolating propositions that hold for formal reasons from those whose proofs require techniques particular to a given mathematical discipline”—seems to align with the latter opinion. What has in fact happened in recent decades? Has category theory turned out to be mainly a “simplifying abstraction” as well as an interesting branch of mathematics in its own right? Or has it been used to prove meaty new results in other fields as well?
- bopbeepboop 6y ago
  I’m not familiar with category theory in depth, but homotopy type theory uses category theory for its semantic model and HoTT’s a big deal in the automated reasoning world. > Others thought it was pretty and useful for identifying similar structures in different fields but wasn’t much use for making significant new mathematical discoveries. A sentence in Emily Riehl’s book—“The category-theoretic perspective can function as a simplifying abstraction, isolating propositions that hold for formal reasons from those whose proofs require techniques particular to a given mathematical discipline”—seems to align with the latter opinion. Two points: 1. Being able to “lift and shift” techniques is a big deal in mathematics — so the two cases are the same. A lot of recent innovations are along those lines, where techniques in one area were applied to a new area. In that sense, category theory is wonderful because it gives us a map for how to move techniques around. You could even go so far as to say the algebra-geometry correspondence is category theory’s first “big win”, as it came about as a way to formalize that body of work. 2. Category theory is the native language of data fusion, while categorical syntax is easy to represent in an image-completion kind of way... so category theory is useful for labs working on using machine learning to fuse data and extract semantically meaningful information. Or labs working on an AI model which can suggest improvements to itself.
divbzero 6y ago
> I really enjoyed her talk at lambda world, “A categorical view of computational effects” [1] [1]: https://www.youtube.com/watch?v=Ssx2_JKpB3U https://www.youtube.com/watch?v=Ssx2_JKpB3U
blux 6y ago
Thank you for your comment. This inspired me to try to take another stab at studying category theory. I'll start with this lecture: https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm... Are there any good books you can recommend on the subject?
- omaranto 6y ago
  What book will suit you depends on your background. If you have a solid background in math, say an undergraduate degree in math, my favorite book is Emily Riehl's Category Theory in Context [1] (the "context" in the title refers to a background in math). If you don't know that much math, I'd recommend Tom Leinster's Basic Category Theory [2] or Steve Awodey's Category Theory [3] (particularly if you have some background in computer science or programming). [1] https://math.jhu.edu/~eriehl/context.pdf https://math.jhu.edu/~eriehl/context.pdf [2] https://www.maths.ed.ac.uk/~tl/bct/ https://www.maths.ed.ac.uk/~tl/bct/
  - blux 6y ago
    Thank you for the pointers.

jamiek88 6y ago

What was the number one thing about category theory that changed your perspective if you don’t mind me asking? You seem very enthusiastic and I’d like to share that enthusiasm one day.

bopbeepboop 6y ago
Not the person you’re asking, but the “aha” moment for me was connecting whiteboard diagrams with type theory. Whiteboard diagrams work because they’re a categorical diagram related to the semantics of the program I’m trying to write. In the sense that CT and TT are “equivalent”, your whiteboard diagrams are your program.
type_enthusiast 6y ago
For me, it was realizing that category theory is the mathematical language of abstraction – almost literally the "principle of least power" in math – and those abstractions often connect to programming abstractions. Even if you're not using words like "Functor" or "Monad" to describe them! And it can be useful to think of them more abstractly than they actually are, even if you're not going to use them that way (or even talk about them that way in your code). Just making some "ridiculously abstract" connections can help provide a missing piece of architecture, even if you keep the math story to yourself (which you likely should). So it can (potentially?) be useful to model various things in terms of what they mean "at the most abstract level", and then find ways to capture chunks of that into various architectural abstractions that make sense without category theory (kind of like a Karnaugh map, in a sense). Sorry if that seems like a lot of "purple prose" or self-important... it really isn't. I think it's the same thing that a lot of people mean when they say "I don't use Haskell but learning it made me a better programmer." I don't use abstract algebra, but learning it made me a better programmer (those statements might even be homomorphic, depending on the Haskell involved)
chas 6y ago
The first thing that got me really enthusiastic in category theory was seeing the definition of the categorical product in terms of universal properties. It's a very simple, but very different way of defining objects that makes it easy to see the relationships between similar objects in different contexts. For example, multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming are all products in particular categories* and the universal property definition unifies them very nicely. There isn't really enough space here to spell it out in detail, but this[0] is a good explanation. There is also a very natural way to manipulate the definition (categorical duality) to get coproducts which unify things like logical disjunction (||), greatest common divisor, and disjoint union of sets. This extremely unified view is also nice because if you have an unfamiliar mathematical or computational object, but you know that it has a categorical product, you suddenly know a ton about what you can do with it as well as some interesting questions to ask and properties to go looking for. This genre of abstraction is all over the place in category theory and it gets way more interesting, but seeing products defined like this and how incredibly unifying of an abstraction it is was the first place that I really saw what the categorical perspective brought to the table. *Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about the action on objects), least common multiple within the category of positive integers ordered by divisibility (a partial ordering being just a special kind of category), logical conjunction within the category of truth values (which can be thought of as sets with at most one element), and structs or record types in the category whose objects are the types of your favorite programming language and morphisms are the programs between them. (From Chinjut, last time I brought up categorical products on hn: https://news.ycombinator.com/item?id=8780786 https://news.ycombinator.com/item?id=8780786) [0] https://rnhmjoj.github.io/category-theory-for-programmers/src/part-1/chapter-5.html https://rnhmjoj.github.io/category-theory-for-programmers/sr... If you'd to see how this applies more directly to programming, work like this is a direct application of the same definitional strategy for abstraction: https://blog.sumtypeofway.com/posts/introduction-to-recursion-schemes.html https://blog.sumtypeofway.com/posts/introduction-to-recursio...
adamnemecek 6y ago
For me it was the idea of adjoint functors which is the central idea of category theory. I wrote up a bit on it here https://github.com/adamnemecek/adjoint https://github.com/adamnemecek/adjoint

mauflows 6y ago

What are your favorite books on the topic?

KirillPanov 6y ago
Steve Awodey's Category Theory, hands down. https://www.goodreads.com/book/show/2047855.Category_Theory https://www.goodreads.com/book/show/2047855.Category_Theory It's a mathematics book written by a philosophy professor that is extremely readable for computer scientists. Very CMU, much wow, such deduction.

tkgally 6y ago

I had a brush with category theory more than forty years ago. I got a master’s degree in math at the University of Chicago in 1980, Saunders Mac Lane was on the faculty, a few grad students were doing category theory, and I worked through part of Mac Lane’s Categories for the Working Mathematician on my own. I left mathematics soon after—with some regret—and haven’t kept up with the field. The interview with Emily Riehl and the introduction (which I read just now) to her book Category Theory in Context suggest that the field has made a lot of advances in the years since. I have a question for people who are familiar with recent developments. Forty years ago, the opinions of other math grad students about category theory were divided. Some thought it had the potential to yield great breakthroughs and solve previously unsolved problems in many branches of mathematics. Others thought it was pretty and useful for identifying similar structures in different fields but wasn’t much use for making significant new mathematical discoveries. A sentence in Emily Riehl’s book—“The category-theoretic perspective can function as a simplifying abstraction, isolating propositions that hold for formal reasons from those whose proofs require techniques particular to a given mathematical discipline”—seems to align with the latter opinion. What has in fact happened in recent decades? Has category theory turned out to be mainly a “simplifying abstraction” as well as an interesting branch of mathematics in its own right? Or has it been used to prove meaty new results in other fields as well?

bopbeepboop 6y ago
I’m not familiar with category theory in depth, but homotopy type theory uses category theory for its semantic model and HoTT’s a big deal in the automated reasoning world. > Others thought it was pretty and useful for identifying similar structures in different fields but wasn’t much use for making significant new mathematical discoveries. A sentence in Emily Riehl’s book—“The category-theoretic perspective can function as a simplifying abstraction, isolating propositions that hold for formal reasons from those whose proofs require techniques particular to a given mathematical discipline”—seems to align with the latter opinion. Two points: 1. Being able to “lift and shift” techniques is a big deal in mathematics — so the two cases are the same. A lot of recent innovations are along those lines, where techniques in one area were applied to a new area. In that sense, category theory is wonderful because it gives us a map for how to move techniques around. You could even go so far as to say the algebra-geometry correspondence is category theory’s first “big win”, as it came about as a way to formalize that body of work. 2. Category theory is the native language of data fusion, while categorical syntax is easy to represent in an image-completion kind of way... so category theory is useful for labs working on using machine learning to fuse data and extract semantically meaningful information. Or labs working on an AI model which can suggest improvements to itself.

divbzero 6y ago

> I really enjoyed her talk at lambda world, “A categorical view of computational effects” [1] [1]: https://www.youtube.com/watch?v=Ssx2_JKpB3U https://www.youtube.com/watch?v=Ssx2_JKpB3U

blux 6y ago

Thank you for your comment. This inspired me to try to take another stab at studying category theory. I'll start with this lecture: https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm... Are there any good books you can recommend on the subject?

omaranto 6y ago
What book will suit you depends on your background. If you have a solid background in math, say an undergraduate degree in math, my favorite book is Emily Riehl's Category Theory in Context [1] (the "context" in the title refers to a background in math). If you don't know that much math, I'd recommend Tom Leinster's Basic Category Theory [2] or Steve Awodey's Category Theory [3] (particularly if you have some background in computer science or programming). [1] https://math.jhu.edu/~eriehl/context.pdf https://math.jhu.edu/~eriehl/context.pdf [2] https://www.maths.ed.ac.uk/~tl/bct/ https://www.maths.ed.ac.uk/~tl/bct/
- blux 6y ago
  Thank you for the pointers.