Can someone explain to me why there are so many category theory posts in HN? To me it's just a pretty obscure branch of mathematics and there are almost no posts about any of the more popular branches of mathematics.
You don't believe me? Read the ICM proceedings https://www.mathunion.org/icm/proceedings and count how many times the words "category" or "functor" appears. And notice something very special, too: you'll find articles that are not about category theory per se, and that will still mention categories. And you know what? They don't even explain what they are. You know how that can be? Categories are so pervasive in mathematics. You wouldn't write an article for the proceedings and explain what a group or a vector space is, would you? Well, same for categories. It's a basic (in the original sense of the word) part of mathematics.
So I'm curious as to how exactly you disagree: the existence of connections between CT and other fields are objectively and verifiably well established (just read a randomly-selected CT paper!) but perhaps you feel like the categorifications of other fields are incomplete or unrepresentative? Or that the connections are in some sense forced or unnatural?
I don't think that there are as many and as important as they claim, and I don't think that several fields use them (yet). Sure, CT advocates have huge lists of unifications and connections (e.g. categories for the working mathematician has a lot), but they don't appear on the other side. Maybe they will, but I don't think they do yet. Thus the 'obscure'.
Thank you for explaining :)
And Hacker News was started as a discussion site to attract that kind of person here to where they would all become aware of each other, aware of Y Combinator, and aware of the opportunities to have from starting startups.
The community of people here expanded out from that core. But category theory is pretty close to that original core, and so it isn't a surprise that it gets more attention here than elsewhere.
The trias gives extreme scope for technology transfer between mathematics, logic and programming.
Type theory? Sure. Logic and model theory as well. Set theory? Number theory? Heck, even geometry is used for dozens of algorithms, not related to geometry (convex optimizing in an n dimensional space, Hamming distance, abstract convex geometry etc). But category theory? Do you have any influential papers or books in mind?
I do think "extremely influential" is overstating it. Outside of that, plus some niches of niches of academic CS, I can't really think of any other places where category theory is particularly important.
[0] Eugenio Moggi Computational lambda-calculus and monads (1989) https://www.cs.cmu.edu/~crary/819-f09/Moggi89.pdf
More vaguely but also more sweepingly I think the general approach, now the standard in language design, of taking a pure language as base and then adding effects to it is established thanks to Moggi's work on monadic effects, which makes essentially all modern programming languages heavily influenced by CT (at a couple of steps' removal).
The theory of (Moggi) monads and monad transformers has been influencing modern programming (and libraries) very heavily (e.g. all of Haskell, Scala's ZIO vs Cats, Rust approach to returning errors). Most modern programming language research engages in some form or other with linear types (and its relatives, like affine) and they come from Girard's linear logic. Both (Moggi) monads and linear logic are heavily influenced by their inventors learning of category theory. So I'd say, whenever you program in a modern language or use modern library design, you (indirectly) stand on the shoulders of many giants. Some of those giants were category theorists.
Interestingly, what I'm beginning to detect is an influence of computer science on category theory, if only because we want to verify abstract maths in automated tooling.
Rust's types evolved over many years. Rust used to have "typestate" for example. I had discussions with Graydon Hoare around 2011-ish about session types (which are linear). It struck me that Hoare knew exactly what I meant with the term. More generally, linear typing was just "in the air" in the early 2000s: you could not been serious in programming language design without being aware of linearity. Linearity was all over the research literature. Hoare was clearly very knowledgable in programming language research.
Girard mentions the connection with categories all the time.
For example in "Proofs and Types" he proves various theorems along the lines of: the sub-category of coherence spaces and stable maps (one of the main models that LL was developed for) induced by some LL fragment is cartesian closed category (IIRC). I think he developed LL in parts by fine-tuning it, until all the categories induced as models of fragments of LL have nice categorical properties. (To the extent that is possible.) When I was a PhD student, my supervisor suggested that I learn category theory to understand linear logic. (Not sure, in retrospect, that was the best course of action, but that was my trajectory)
There is a thriving ‘school’ of computer science that views category theory as the third leg of the category theory, type theory, proof theory triangle that forms their basis for all computer science. This is very evident in the CS department at Carnegie-Mellon. If you are interested I’d recommend checking the backlog of lecture videos and presentations at the Oregon Programming Language Summer School program.
citation please? there's one guy in my department (one of the best theory departments in the US) that contributes to sml and that's about it as far functional goes.
a less charitable/more accurate response to gop's question is: HN has a fetish for both functional programming and cat theory. there's even another response here that captures the sentiment beautifully:
> I have studied math and was in some lectures about category theory. I still don't get what the project is about and that fact intrigues me.
Cat theory is something else: https://news.ycombinator.com/item?id=37685885
- Large research area
- Definitions you can comprehend without a math background
- Extremely vague applications so that there's no area in which it definitely doesn't apply.
I think the hype, which has lasted for a decade now, is a result of there being a lot of smart people in different fields who are interested in math research, but not so interested they're going to catch up to whatever the Langlands program is about.