Question to all CS majors, that invested in learning Category Theory:
Did you have any concrete take aways from learning it?
( I have a math background, and struggle to find something concrete. Maybe I am just blind. )
Did you have any concrete take aways from learning it?
( I have a math background, and struggle to find something concrete. Maybe I am just blind. )
Other maths courses do this as well, but real analysis is particularly vivid for some people because of all the fun counter-examples you get to see in a well-taught course, such as a function that is everywhere continuous but nowhere differentiable.
This habit of thinking through corner cases is something I miss from a lot of (junior) programmers.
Edit: More: The connection between type theory, logic, and computation is not specious, but is part of the fabric of reality. I now can understand why chemistry -- being a linear logic -- is time-reversible, or why every DAG is a poset is a system of logic is a language of computation, or why a ring has two interlocking groups, or why social groups tend to include one big conversation and many side chats in a power-law distribution of sizes.
i think gp might have been asking about practical use in CS ( CS majors).
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.
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 know a thing or two about the prevalance of categories in Mathematics (https://arxiv.org/abs/1012.3121).
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."