Because people think “category theory” means “abstract math” in general, due to cargo-culting in and around the Haskell community.
There's a lot of empty posturing by people who don't really seem to understand a lot of mathematics but still seem to have very strong convictions about certain aspects of it (constructivism is another such thing).
I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof."
To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system.
Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.
Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it.
But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen some NJ Wildberger video where he shittalks the real numbers.
So it's not even just constructivism per se, more this mix of unprincipled finitism + constructivism + no axiom of choice (or any mixture thereof), as opposed to anything grounded in some rigorous methodology. Basically the "I don't understand set theory or logic but I've heard that Banach Tarski is weird, so mainstream mathematics must be full of shit".
You'd think people wouldn't have hot takes about mathematics, but somehow they do.
As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.)
But can we agree to both dislike people who argue that 0.999... is not 1?
And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").
As for choice, try doing much functional analysis without Zorn's lemma.
There are parts of math that you can do constructively. But most of it you really can't. And choice is embedded in a lot more math than you'd guess.
Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsense. In many ways, it ought to be a lot easier for someone committed to constructivist semantics to grok a classical development than the converse - because decision procedures, computations etc. are way more of an afterthought to mainstream mathematicians.
But I'm also a strict formalist, or more accurately, I think whichever axioms happen to be useful should be used, without much need for there to be a epistemological commitment.
I can see why categories appeal if you're just looking at definitions, but CT often just abstracts/standardizes an approach that folks were already working with when working with rings, groups, topologies, etc. Going through the proofs will teach you when to apply what.
Aluffi (Algebra: Chapter 0) makes a great book that teaches the basics of CT and brings it up while teaching regular algebra. I highly recommend it.
In parallel I developed this very "visual" way of thinking about structure that makes me really resonate with CT. In a way I'm less interested in learning new maths, more so than learning more about how people approach (complex) structures I already know with these very rudimentary concepts, and seeing how their formalizations match my "folk mathematics".
I'm having a lot of fun!
edit: thanks for the book recommendation! that looks like my kind of maths book
I also like the focus on quotient groups and galois fields, as well as using graphs as recurring examples, which have been the only times I really put the pedal to the maths metal in my programming (for some crypto and error correction stuff).
Looking at it now, I think maybe I just found it too boring to remember the tricks, and too tedious to not make mistakes, while I found coming up with proofs more "interesting" and requiring less rote memorization.
I wish the university calculus changed the curriculum. I didn't find it particularly useful to learn how to integrate e.g. inverse trig given that WolframAlpha exists. There are lots of other examples of teaching memorization of silly tricks like that. I guess they probably do it because it's easy to test.
While I only got so far in proving stuff about a cyber-physical I was working on, but this was really fun to learn: https://github.com/LS-Lab/KeYmaeraX-release
See also: http://lfcps.org/lfcps/
I found groups, limits, continuity, fields to be much more amenable to my thinking. It felt way more similar to the things I really enjoyed (building software in scheme and C and writing exploits in assembly).
For me, I realized thst I need to write the code to accompany the maths, because it helps me disambiguate mathematical notation and put "types" on things.
It helped me a lot to work alongside real maths PhDs and realize that they have a very "intuitive" approach to maths, and don't necessarily yeet lemmas and proofs around all day, instead spending a lot of time brainstorming on the whiteboard and discussing things out, very similarly to software design. It was one of them telling me that my thinking was very mathematical that helped me "deconstruct" the fear of maths that I had built up.
I myself find beauty in some parts of analysis, but algebra definitely speaks more to me (e.g. I find a proof of Lagrange's Theorem more beautiful than one of the Intermediate Value Theorem). So I can relate.
(we don't talk about the topologists)
Logic and proof theory is actually one of the areas in math where category theory is most clearly useful. Intuitively, this is because reflexivity ("A leads to A") and transitivity ("A leads to B and B leads to C, hence A leads to C") are well-known rules of any kind of proof writing or indeed of argumentation in general, and they exactly describe a category.
As someone familiar with algebraic objects and relations etc., I don’t see what category theory is adding in terms of practical usefulness in software development.
Also, reflexivity, transitivity and symmetry just define an equivalence relation, no need for CT there.
Eg Stuff about types and endofunctors feels like trivial examples using the jargon just to use it. OTOH discovering the Top->Grp functor in algebraic topology is kind of unexpected and revealing.
For example if it were 2008 and you want to be inventor Applicative functors for use in Haskell, then knowing lax monoidal functors from CT might be helpful. But if you want to just use Applicative functors, you don't need to learn lax monoidal functors first.
So programmers probably don't need to learn CT because they can just let the computer scientists devise their abstractions for them. But if you want to be a computer scientist and one day devise your own abstractions[0], then maybe CT would be helpful.
Your description is the single best sales pitch for learning it that I've ever heard. I'm legitimately interested now — in a way that I simply wasn't before your comment.
Everyone else who tries to hype up CT is always like, "Whoa, bro, don't you know that addition is actually a monoid endofunctor over the set of all hyper-reals?" (Or something.) I guess that sort of breathless mathematical revelation is supposed to be so mind-blowing that anyone who hears it gets instantly hooked. My usual response was always just, "So what?"
But you're telling me I can become a better engineer? A meta-engineer, who can engineer things to engineer with? Yeah, I'd definitely be up for that.
https://corecursive.com/050-sam-ritchie-portal-abstractions-...
I think I might have linked it in the article.
That said, if I had to guess at what would be effective at getting up to speed without spending 25 years, would be to checkout https://github.com/hmemcpy/milewski-ctfp-pdf Category Theory for Programmers. Milewski was one of those people who were like "Oh, it's simply Yoneda this and Yoneda that", and he figured it out all himself in parallel without seeing my proof.
But I doubt it will be like, knowing Category Theory will enable you to have super powers for abstraction design. Rather it will be a matter of having enough mathematical tools at your disposal plus the right inspiration at the right time to realize that ones of those tools can happen to solve your abstraction programming problem you happen to be facing at some moment, in a way that is not obvious, if you are lucky. In fact, you likely have to first guess at what the right abstraction is and then fall back on Category Theory to verify the sanity of your guess.
Independent of mathematical numerical systems used, everthing gets loaded at hoursX0000. Everything else after that is just bracket arrangements.
If let things stack up, then it's all about what can be accomplished before zeroing out.
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
Maybe I'm missing something but it seems to me that all you can study monads in programming languages without having to also learn the category theory abstraction of it. The same goes for semigroups, monoids, folds, functors, ...
I'm sure there's a benefit in category theory once you want to unify all these abstractions and talk about all of them together, but I see so many people who think they have to learn CT before they can understand monads in e.g. Haskell, and I don't really understand why.