I heared many people talk about Haskell, Monads and Types <=> Proof duality, but I never heard anyone saying: "I applied the Yoneda Lemma to build this API.", or "I read about Category Theory and now $CONCEPT_XYZ started making sense to me."
And CS is merely a subfield of maths. What should I say? Scott theory, domain theory, CPOs, Galois connections? The problem here is that, as usual, folks are trying to figure out what category theory is good for, but ignoring the entire point: The definitions are the important part. Once the definitions make sense, then the rest of the system makes sense. Category theory is all about the definitions, and moreover, all about coming to have the definitions at hand so that one can recognize categorical structures in practice.
Or, I guess, I could take a lazy route and just say "theorems for free, those are the practical use" and be done. But it's frustrating to hear folks over and over wonder what something is good for, when they clearly aren't reading and trying to find the goodness for themselves.
The problem for someone like myself is that I have taken some classes on basic abstract algebra in high school (groups, monoid, rings etc) and came out of it with some definitions and... Nothing else. I can probably still tell if some operation on some set forms a group or not, but that has never been a directly useful tool in what I learned further through high-school and university. It didn't help in linear algebra. It didn't help with calculus. It didn't help with control theory. It didn't help with numerical methods. Sure, I could go around and see if new operations I learned about formed, say, rings, and I'm sure a lot of them do, but that was never used in theorems or demonstrations in those fields (the way I was taught them, anyway).
It was only ever a set of definitions. And almost everything I've seen browsing on category theory seemed the same - like it's just definitions, new names for old concepts, with few theorems shown that elucidate the need for these new names.
For example, lists and optionals and Either are monads. IO is also a monad. The most I've seen make use of knowing this fact is some nice-ish syntax sugar that works for all 3 of these seemingly disparate concepts. But even then, the 'work' for enabling that sugar seems to be done by the simple properties of the monad, more than some theorem that had been proven on monads in general.
Are there some examples of common CS abstractions that are almost but not quite category theory constructs? Are there any simple examples where we get new proofs by recognizing that some old CS concept is, say, a monad?
I understand your point about theorems for free in principle, but I have never seen one in these kinds of discussions (at least, not one that wasn't also a definition, e.g. if X is a monad than Y must be a functor).
i think gp might have been asking about practical use in CS ( CS majors).