What's category good for? It's a serious question so please don't say "monads", I understand monads just fine without knowing category theory. I'm down to put in the work if the reward is there.
First the joke answer. In mathematics, once you understand the proof of something, we say that it is trivial. Category theory is about making things trivially trivial.
Now the serious answer. Category theory is about abstracting away the details of mathematical domains so that fundamentally parallel proofs and constructions can be seen to be essentially the same. It also allows you to create constructions that allow problems in one field to be transformed into problems in an apparently unrelated one where you might find them easier to prove.
The result is that in a new field, you recognize the category and suddenly have a whole bunch of results, and some important constructions to look at. Such as the tensor product.
And in existing fields you can do things like use homotopy theory to turn topology problems into algebra problems, where they are often easier.
Imagine if you took a mathematical construct and replaced all of the familiar terminology with gensyms. For example:
"A florb is brazzle of carnatious snoggles. A florb is itself a snoggle and so can be a fnizzle of another florb."
This is actually the definition of what is normally called (in English) a SET, under the following mapping of vocabulary:
florb = set
brazzle = collection
carnatious = distinct
snoggle = object
fnizzle = member
Category theory is about extracting the fundamental structure of mathematical definitions so that these kinds of equivalences can be studied with mathematical rigor.
I agree with others that this comment has increased my understanding greatly. Perhaps since this is a linguistic example, it resonates. Thank you for replying.
Not a clue. I don't actually know much at all about category theory, just enough to offer up that explanation of what it's about. And I had never heard of Attempto before you mentioned it.
I'm kind of surprised no one has said this, and I'm kind of a novice, so I'll probably get it wrong.
To me, the interesting thing about category theory is that it draws out the significance of relationships in a system. We often spend a lot of time thinking about the things, themselves, in a system.
- What are their properties?
- What do they mean?
- What is their identity?
In category theory, almost all the significance of individual things is erased. Instead, you often group things up into sets and other structures, and then call the whole set an object. Then you think about the existence of morphisms from one kind of object to another. A morphism is kind of like a function, in the sense that something goes in, and something else comes out. Except that we're not concerned about the properties of what's going in and coming out, so the function body doesn't really matter. A morphism is something more general than any specific function. It's more like a function declaration--specifying that something does exist without saying anything concrete about what it does.
So, you're operating on a level of abstraction that removes basically all unnecessary details about things and relationships, other than existence and some basic rules for how those relationships can be composed to form new ones. As it turns out, there's a whole lot you can say and prove about categories once you know a bit about their structure.
In my opinion, the real power is that any given system can often be "projected" into categories in a multitude of different ways, and depending on the structure of those categories, you can say apply proofs from category theory to say interesting things about that system.
Going further beyond that, category theory concerns itself with how categories relate to each other, by considering categories themselves as objects and relationships between them as morphisms.
Why does this matter to programmers?
Well, we often want to design systems that are predictable, no matter what the actual identity of the data that traverses them. This is abstraction, and we do it on many levels, all the time. We also want to chain together our abstractions. This combination of abstraction and composition is something category thoery is well suited to analyze.
I'm probably off here in some important ways, but this is my layperson's takeaway from spending some time trying to understand what all the fuss was about.
To really drive the point home of the level of abstraction I like to think of a category of domino tiles.
It kind of makes a few things apparent.
Tiles would be the morphisms and objects would be the number spots on the tile ends.
So the first insight: morphisms is the actaul object of study. The “objects” of a category is just a consequence of how the morphisms may, or may not, compose.
My first hurdle when learning things was being distracted by trying to understand what objects where, some times they would be types, sometimes sets, and it was never really clear what their cardinality would be. As if the theory hid important details that you had to keeps track of implicitly. But it doesn’t, objects really are inconsequential, they are just there to be a place for morphisms to meet, nothing more. Just like the number of dots of the domino tiles. We could have used color instead, and the tiles would compose in exactly the same way.
Second intuition, there’s no computation or anything else going on. Just as you say about the functions. The only thing of concern are the composability of those things called morphisms, be they functions or domino tiles.
In the lecture series linked a few places in this thread, Bartosz makes a fantastic point of this when deriving some properties of surjective and bijective functions using only composability.
Well, monads in programming are modeled on category-theoretic monads, so you do know a bit.
Monads, functors, arrows, etc are just patterns that show up a lot in functional programming that also happen to have analogues in category theory. This isn't too surprising, because category theory basically started from mathematicians trying to formalize common patterns in disparate areas of math. Categories pop up all over the place in math, and math of course is the main abstraction that we formally model just about anything in reality.
Given how ubiquitous they are, I think it's worth it to have a working, informal knowledge of category theory. It doesn't take serious time or study to do that.
I think the idea is that it abstracts away a bunch of the area-specific stuff from other fields, distilling it all down to generalized reusable concepts. For instance, I watched the first lecture and saw immediate connections to the compatibility matrices used in programming language analysis and type theory. I didn't "learn" anything new from the lecture (it was all introductory), but I'm sure that if I keep up with the future lectures I'll see more that I can actually apply to my work.
Example: the first question on the first problem set [1] shows how the idea of the Least Common Multiple and the Greatest Common Divisor are analogous to ⊤ and ⊥ in PLT, or "any" and "never" in TypeScript. (Specifically, the Join and Meet operations)
LCM and GCD are meet and join (union supertype and intersection subtype in PLT), not top and bottom. Top/any would correspond to the product of all numbers (union of all factors), and bottom/never would correspond to 1 (intersection of all factors).
Oh right, "Lattice" is the word I was looking for. It's been too long. Would that be considered a subset of category theory, a precursor to it, or another field that it somewhat "unifies"?
I don't know much about CT, but I believe that if you want to work with Higher Kinded Types, you'll keep going back to ideas related to CT (functors, endofunctors, natural transformations...).
I'm not sure if taking a course in CT is the most efficient way to learn how to apply such concepts in computer programming, thought. Maybe someone with more experience can give it's opinion.
One thing it can be used for is to prove certain propositions that might otherwise be hard to get traction on.
Its concepts are so abstract that many different things can map to them. So if you can prove that something is a group, or a monoid, or whatever, then by the rules of category theory, you can now prove certain characteristics of that thing. This could wind up being a vital step in a longer proof.
When this happens, it usually feels like you moved your proof forward without actually gaining any new understanding (because the concepts are so abstract). Therefore, this is often referred to as "general abstract nonsense," but in a tongue-in-cheek manner, because you actually did derive concrete value.
To a programmer, the real nuts and bolts of category theory aren't a ton of use. People have had some success reverse engineering some of these concepts into programming technologies, but it is a very long road to learn enough CT to either replicate or benefit from that road.
There's also the regular misinterpretation that mathematical objects like, e.g. monoids, are well understood through CT. That's pretty false. There's the "intermediate level" of abstract algebra where you can study these objects and the world they live in much more directly and immediately. There's some real benefit from learning some parts of abstract algebra. Trying to learn CT in order to learn abstract algebra is complete overkill, though.
In both of these cases, my advice boils down to "just learn the things you're interested in directly as opposed to 'via' CT". That's because CT is really what happens when you boil and boil and boil away these different fields and are just left with some very universal ideas. Abstract nonsense.
If you're a mathematician and these concepts are your daily bread and butter... hey, you might still not want to learn CT because it's better to just work with what you're studying directly.
Okay, objections and disclaimers over. The thing you can learn from CT which is interesting and valuable is the very powerful, universal perspective of "if you want to understand something, look at how it relates to other things". Category theory is absolutely focused on this idea and most of its insight is that this idea, taken in its extreme, is extraordinarily far reaching.
Again, you can probably learn this more practically by studying where it shows up in something you actually care about. It won't be a theorem there, but instead just sort of "in the fabric" of the field, a major technique used in proofs. CT is nice because it unified those "folk theorems" from all over mathematics.
More relevantly, in programming the CT perspective lies close to the FP perspective where "transformations" of data and "pipelines" are given center stage as opposed to "objects" and "procedures". It's also embedded in ideas of domain specific languages and both concrete and abstract interpretations, thereof.
Most likely, you want to learn the actual techniques of interest and then maybe later just learn a bit of CT to get a sense for "how they all connect". I think there are opportunities for CT to influence your programming if you were to become familiar with it, but they're still kind of fuzzy today.
Finally, if you want to learn CT I recommend you learn abstract algebra first via Aluffi's "Algebra: Chapter 0". It's secretly a CT book, but is not trying to be so abstract. You can also learn a lot from Schanuel and Lawvere's "Conceptual Mathematics" which, I feel, is one of the better books for establishing the "category theoretic POV".
Differentiation (of functions) is a product-preserving functor, which makes the Chain Rule the rule by which it respects function composition, which makes automatic differentiation a matter of writing out the syntax tree of functions and "folding it up" via a catamorphism (a generalized fold).
If you find that being able to answer a high enough number of assignments you know that the course is for you. If not, the lectures may still be of interest, but it is much less likely the less of the assignments you think are worthwhile for you.
PS: Question 4 in problem set 3 is quite (in)famous :-) Just the headline:
> Question 4. A monad is a monoid in a category of endofunctors (harder/optional)
So, if you want to be one of the few people who actually understand that sentence when it is quoted as a joke (usually in programming forum whenever monads come up), this is your course.
Category theory is a relatively new branch of mathematics that has transformed much of pure math research. The technical advance is that category theory provides a framework in which to organize formal systems and by which to translate between them, allowing one to transfer knowledge from one field to another. But this same organizational framework also has many compelling examples outside of pure math. In this course, we will give seven sketches on real-world applications of category theory.
Category theory is a relatively new branch of mathematics that has transformed much of pure math research. The technical advance is that category theory provides a framework in which to organize formal systems and by which to translate between them, allowing one to transfer knowledge from one field to another. But this same organizational framework also has many compelling examples outside of pure math. In this course, we will give seven sketches on real-world applications of category theory.
Category theory is like putting types around mathematics. Like how dimensional analysis in physics points the way toward what operation to perform, category theory helps to show what mathematics "makes sense". Another example: I've heard that Haskell's type system is so good that you can often find the function you need just by searching for the function signature (it's type). Category theory does that for mathematics.
They say that "mathematicians are people who like calling the same name to different things". Category theory generalises and abstracts many different concepts and shows that they are actually the same thing in categorical theoretical terms.
The idea is that it's a language for abstracting out common type relationships and calculations. I haven't yet seen a software-development context where those abstractions carry their weight, though.
It is only useful in languages
with sufficiently expressive type systems, like Haskell. Otherwise you quickly hit a wall where it's impossible or impractical to express your idea in the language's type system, the same complaint that python programmers have when they try to write Java.
Are you asking whether it has beneficial features that Set Theory doesn't have (it does)? Or are you asking for examples of useful application (which there are a number)?
Or are you asking for examples of useful application such that category was absolutely necessary?