What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
What's the thing with category theory? I see this topic discussed quite frequently here but I don't get it why people are so into it
Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe. At first this might seem a perverse thing to do as mappings seem more complex than sets, but that is just because traditionally mappings have usually been defined in terms of sets.
In set theory you can specify that two sets be equal and you can also specify that one set be an element of another.
In category theory you can specify that two mappings be equal and you can also specify that two mappings compose end to end to produce a third mapping.
Category theory can be used to express some requirements in a very concise way.
> Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe.
I'm not sure about that, because you still need some concept of set (or collection or class) to define a category, because you need a set of objects and mappings between them (technically that's a "small" category, but to define any larger category would require at least as much set-theoretical complication).
More exactly, whereas in set theory it's the membership relation between sets and their elements that is basic, in category theory it's the mapping between objects.
Nevertheless, the basic concepts of set theory can also be defined within category theory, so in that sense they're inter-translatable. In each case though, you need some ambient idea of a collection (or class or set) of the basic objects. Tom Leinster has a brilliantly clear and succinct (8 pages) exposition of how this is done here https://arxiv.org/abs/1212.6543
The thing is, even defining first-order logic requires a (potentially infinite) collection of variables and constant terms; and set theory is embedded in first-order logic, so both set theory and category theory are on the same footing in seemingly requiring a prior conception of some kind of potentially infinite "collection". To be honest I'm a bit puzzled as to how that works logically
Defining first-order logic doesn't really require set theory, but it does require some conception of natural numbers. Instead of saying there's an infinite set of variables, you can have a single symbol x and a mark *, and then you can say a variable is any string consisting of x followed by any number of marks. You can do the same thing with constants, relation symbols and function symbols. This does mean there can only be countably many of each type of symbol but for foundational purposes that's fine since each proof will only mention finitely many variables.
Allowing uncountably many symbols can be more convenient when you apply logic in other ways, e.g. when doing model theory, but from a foundational perspective when you're doing stuff like that you're not using the "base" logic but rather using the formalized version of logic that you can define within the set theory that you defined using the base logic.
Thanks, that sharpens it then to a question about natural numbers, or at least some idea of an indefinitely extensible collection of unique elements: it seems the ordering on the numbers isn't required for a collection of variables, we just need them to be distinct.
I don't think you need set theory to define set theory (someone would have noticed that kind of circularity), but there still seems to be some sleight of hand in the usual presentations, with authors often saying in the definition of first-order logic prior to defining set theory that "there is an infinite set of variables". Then they define a membership relation, an empty set, and then "construct the natural numbers"... But I guess that's just a sloppiness or different concern in the particular presentation, and the seeming circularity is eliminable.
Maybe instead of saying at the outset that we require natural numbers, wouldn't it be enough to give an operation or algorithm which can be repeated indefinitely many times to give new symbols? This is effectively what you're illustrating with the x, x*, x**, etc.
If that's all we need then it seems perfectly clear, but this kind of operational or algorithmic aspect of the foundation of logic and mathematics isn't usually acknowledged, or at least the usual presentation don't put it in this way, so I'm wondering if there's some inadequacy or incompleteness about it.*
So category theory is really the theory of composition of mappings. I conjecture that all programming can be seen as just the composition of mappings. If this is correct then category theory is a theory of programming.
It can very much be. Here’s one example of this phenomenon (there are many others but this is the most famous): https://wiki.haskell.org/Curry-Howard-Lambek_correspondence
You don't need category theory to connect dots with arrows, graph theory is enough for this.
Category theory is actually a ‘simplified’ graph theory, i.e. you can see categories as a restricted class of graphs. E.G. ‘Category Theory for Computing Science’ introduces categories this way (a category is a directed graph with associative composition and identity; the free category on a graph is the graph with all identities and compositions filled in). But the restrictions (associative composition and identity) are harmless and natural for programming applications where there's always a notion of ‘do nothing’ or ‘do one thing after another’, and unlock a lot of higher structure.
But what's the utility of this definition? Does it help solve or prove something?
It helps you build an intuition for categories, if you're used to graphs :)
If you have a working intuition for categories then in most cases the specific formulation you choose as a foundation doesn't matter, just as most mathematicians work nominally in set theory without worrying about the subtleties of ZFC.
IMO the right intuition about a tool comes from applying it in the context where it provides a real leverage. In case of Category Theory that would be advanced algebraic topology (not re-phrasing basic things which are easier to understand without CT).
If you allowed infinite graphs maybe. How would you define a functor or natural transformation in graph theory? Seems like you would need to construct a conceptual system that is just equivalent to category theory
No, but if you want to talk about composing those arrows (and a sensible notion of composition should probably be associative, and perhaps have a unit) you eventually end up reinventing category theory.
> you can also specify that two mappings compose
Two mappings with corresponding domain/codomain have to compose by definition of a category. It's not something you can specify.
Yes. When you are specifying a system you are building the category that you want it to live in.
That is probably what they mean by specifying that they compose.
If all you know is that you have two mappings you don't know they compose, until you get the additional information about their sources and targets. In a way that's what the source and targets are: just labels of what you can compose them with.
> Category theory can be used to express some requirements in a very concise way.
Could you give an example in programming, what can be easier expressed in CT than with sets and functions?
It's more that category theory foregrounds the functions themselves, and their relationships, rather than on the elements of sets which the functions operate on. This higher-level perspective is arguably the more appropriate level when thinking about the structure of programs.
For more detail, see Bartosz Milewski, Category Theory for Programmers:
"Composition is at the very root of category theory — it’s part of the definition of the category itself. And I will argue strongly that composition is the essence of programming. We’ve been composing things forever, long before some great engineer came up with the idea of a subroutine. Some time ago the principles of structured programming revolutionized programming because they made blocks of code composable. Then came object oriented programming, which is all about composing objects. Functional programming is not only about composing functions and algebraic data structures — it makes concurrency composable — something that’s virtually impossible with other programming paradigms."
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
> Category theory is what you get when you take mappings instead of sets as the primitive objects of your universe
Why have I never seen it explained like this before. Wow, thank you!
> Category theory can be used to express some requirements in a very concise way.
Can you an example?
Take a mapping a and precompose it with the identity mapping i. By the definition of the identity mapping the resulting composition is equal to a.
(Here ';' represents forward composition. Mathematicians tend to use backward composition represented by '∘' but I find backward composition awkward and error-prone and so avoid using it.)Now, if there is another mapping j that is different from i, such that
then the mapping a loses information. By this I mean that if you are given the value of a(x) you cannot always determine what x was. To understand this properly you may need to work through a simple example by drawing circles, dots and arrows on a piece of paper.If there is no such j then mapping a is said to be a monomorphism or injection (the set theoretic term) and it does not lose information.
This specification of the property 'loses information' only involves mapping equality and mapping composition. It does not involve sets or elements of sets.
An example of a mapping that loses information would be the capitalization of strings of letters. An example of a mapping that you would not want to lose information would be zip file compression.
If you alter the above specification to use post-composition (a;i = a and a;j = a) instead of pre-composition you get epimorphisms or surjections which capture the idea that a mapping constrains all the values in its codomain. I like to think of this as the mapping does not return uninitialized values or 'junk' as it is sometimes called.
Bartosz Milewski works through this in more detail (including from the set-theoretic side) in the last 10 minutes of https://www.youtube.com/watch?v=O2lZkr-aAqk&list=PLbgaMIhjbm... and the first 10 minutes of https://www.youtube.com/watch?v=NcT7CGPICzo&list=PLbgaMIhjbm....
At the 2018(?) ICFP, I sat between John Wiegley and Conal Elliot. They talked about expressing and solving a programming problem in category theory, and then mapping the solution into whatever programming language their employer was using. From what they said, they were having great success producing efficient and effective solutions following this process.
I decided to look for other cases where this process worked.
I found several, but one off the top of my head is high dimensional analysis, where t-SNE was doing okay, and a group decided to start with CT and try to build something better, and produced UMAP, which is much better.
In short, this does work, and you can find much better solutions this way.
(random link https://stats.stackexchange.com/questions/402668/intuitive-e... )
> you can find much better solutions this way
... because mappings map nicely to functions
Category theory gives us a nice, high-level set of conceptual tools to try to understand and generalize over things that are hard to connect otherwise. Some people find that useful directly, other people just enjoy it for its own sake, or even for aesthetic reasons. (I think all three are totally reasonable!)
At the same time, it's actually rather more accessible than most other areas of pure math—at least at the level that people talk about it online. Basic category theory can be hard to learn because it's so abstract but, unlike almost any other are of math from the 20th century onwards, it has almost no hard prerequisites. You can reasonably learn about categories, functors, natural transformations and so on without needing a graduate degree's worth of math courses first. You might not understand the most common examples mathematicians use to illustrate category theory ideas—but it's such a general framework that it isn't hard to find alternate examples from computer science or physics or whatever else you already know. In fact, I expect most of the articles that get talked about here do exactly that: illustrate category theory ideas with CS/programming examples that folks on HN find relevant and accessible.
> You can reasonably learn about categories, functors, natural transformations and so on without needing a graduate degree's worth of math courses first.
This is the whole premise of _Conceptual Mathematics_: category theory for high school students.
Abstract Algebra, looked at through the lens of Programming, is kind of "the study of good library interface design", because it describes different ways things can be "composable", like composing functions `A -> B` and `B -> C`, or operators like `A <> A -> A`, or nestable containers `C<C<T>> -> C<T>`, with laws clearly specifying how to ensure they don't break/break expectations for users, optimizers, etc. Ways where your output is in some sense the same as your input, so you can break down problems, and don't need to use different functions for each step.
Category Theory's approach of "don't do any introspection on the elements of the set" led it to focus on some structures that turned out to be particularly common and useful (functors, natural transformations, lenses, monads, etc.). Learning these is like learning about a new interface/protocol/API you can use/implement - it lets you write less code, use out-of-the-box tools, makes your code more general, and people can know how to use it without reading as much documentation.
Focusing on these also suggests a generally useful way to approach problems/structuring your code - rather than immediately introspecting your input and picking away at it, instead think about the structual patterns of the computation, and how you could model parts of it as transformations between different data structures/instances of well-known patterns.
As a down-to-earth example, if you need to schedule a bunch of work with some dependencies, rather than diving into hacking out a while-loop with a stack, instead model it as a DAG, decide on an order to traverse it (transform to a list), and define an `execute` function (fold/reduce). This means just importing a graph library (or just programming to an interface that the graph library implements) instead of spending your day debugging. People generally associate FP with recursion, but the preferred approach is to factor out the control flow entirely; CT suggests doing that by breaking it down into transformations between data structures/representations. It's hugely powerful, though you can also imagine that someone who's never seen a DAG might now be confused why you're importing a graph library in your code for running async jobs.
Its of course the theory behind monads that since Eugenio Moggi are used to model computational effects in pure functional languages. Effects such as state, optional return types (used in turn for error handling) (maybe monad), input/output (reader writer monad) and others. Beyond effects, Wadler used monads for parsers (monadic parsing).
The Curry-Howard "isomorphism" (slogan: propositions are types, proofs are programs/functions) map code to logic in a categorical way described first by certain book of Lambek-Scott with uses in formal software verification.
Categories provide abstraction. You first distill the behavior of how Haskell (or you other pet functional language) work with Hask, the category of Haskell types, and then you can apply your abstract distillate to other categories and obtain task-oriented, tailored computing concepts that enrich bare language capabilities, providing applications including 1) probabilistic programs 2) automatic differentiation. Conal Elliott has very concrete work along this lines. When he speaks of CCCs (following Lambek) he alludes to cartesian closed categories, the crucial property of having a type constructor for function spaces and higher order functions. See his "compiling to categories" for a very concrete, hands-on feel. Another application he shows is in hardware synthesis (baking your functional algorithm to a netlist of logical gates for automating the design of custom hw accelerators).
In short, why categories? computational effects, formal verification and the equivalence of simply-typed lambda-calculus with cartesian closed categories, with lambda-calculus being the backbone of functional programming language semantics.
I'd phrase this a tiny bit differently: monads give a model of effects in _impure_ languages and are important for that reason. The fact that Haskell chooses to emphasize monads in the language itself is cool, but their utility is not restricted to pure functional languages; quite the opposite! In a pure functional language you don't need to think about effects at all, and the only model you need is mathematical functions, which are much simpler.
one of the things i took away about category theory is that it allows you to avoid repeating certain arguments which boil down to so-called “abstract nonsense” ie they have nothing to do with the specific objects you’re dealing with but rather are a consequence of very generic mapping relationships between them. maybe better versed people can give specifics.
as a very broad example there are multiple ways to define a “homology” (ex simplicial, singular, etc) functor associating certain groups to topological spaces as invariants. but the arguments needed to prove properties of the relationships between those groups can be derived from very general properties of the definitions and don’t need to be re-argued from the very fine definitions of each type of homology.
i think.
Pinging the https://planting.space/ people! I know some of them are on HN, at least recruiting in the past. I haven't updated my knowledge in a while, but my impression of the company was basically that they were going make money using category theory(+all math) in clever and useful ways. I think they turned toward AI a little, but they're at the root a bunch of people who think category theory is useful. Hence, the ping!
Category theory is popular in computer science because, at a fundamental level, they're very compatible ways of seeing the world.
In computing, we think about:
- a set of states
- with transformations between them
- including a ‘do nothing’ transformation
- that can be composed associatively (a sequence of statements `{a; b;}; c` transforms the state in the same way as a sequence of statements `a; {b; c;}`)
- but only in certain ways: some states are unreachable from other states
This is exactly the sort of thing category theory studies, so there's a lot of cross-pollination between the disciplines. Computation defines interesting properties of certain categories like ‘computation’ or ‘polynomial efficiency’ that can help category theorists track down interesting beasts to study in category theory and other branches of mathematics that have their own relationships to category theory. Meanwhile, category theory can give suggestions to computer science both about what sort of things the states and transformations can mean and also what the consequences are of defining them in different ways, i.e. how we can capture more expressive power or efficiency without straying too far from the comfort of our ‘do this then do that’ mental model.
This latter is really helpful in computer science, especially in programming language or API design, because in general it's a really hard problem to say, given a particular set of basic building blocks, what properties they'll have when combined in all the possible ways. Results in category theory usually look like that: given a set of building blocks of a particular form, you will always be able to compose them in such a way that the result has a desired property; or, no matter how they're combined, the result will never have a particular undesired property.
As an aside, it's common in a certain computer science subculture (mostly the one that likes category theory) to talk about computing in the language of typed functional programming, but if you don't already have a deep understanding of how functional programming represents computation this can hide the forest behind the trees: when a functional programmer says ‘type’ or ‘typing context’ you can think about sets of potential (sub)states of the computer.
Still, what's in your opinion, the advantage of thinking in category theory rather than set theory? (For programming, not - algebraic geometry.)
I mean, all examples I heard can be directly treated with groups, monoids, and regular functions.
I know some abstract concepts that can be defined in a nice way with CT but not nearly as easy - set theory, e.g. (abstract) tensor product. Yet, for other concepts, including quantum mechanics, I have found that there is "abstract overhead" of CT with little added value.
In my opinion, the important advantage of category theory over set theory in (some!) computational contexts is that it allows you to generalize more easily. Generalizing from sets and functions to objects and morphisms lets you play around with instantiating those objects and morphisms with a variety of different beasts while maintaining the structure you've built up on top of them, and you can even use it to modularly build towers of functionality by layering one abstraction on top of another, even if you choose later to instantiate one of those layers with good old sets and functions. By contrast, it's hard to imagine treating something like async functions with plain old set theory: while there is of course a way to do it, you'd have to reason about several different layers of abstraction together to get all the way down to sets in one step.
It's just a good set of models to use to think about all sorts of different mathematical systems, kind of like a unified vocabulary. Beyond undergraduate level, category theory these days plays a huge role within many vast fields - e.g., algebraic geometry, algebraic topology, or representation theory.
I think your reply overstates the importance of category theory in mathematics and doesn't give any hint on what it is about.
IMO a better reply would be: category theory appeared to unify the concepts around using discrete objects to prove the properties of continous objects in topology, like fundamental groups, homology groups and homothopy groups. It is only practically useful for very advanced proofs like 2nd Weil Conjecture. Any usage of it in programming is only an analogy and is not mathematically rigorous (see https://math.andrej.com/2016/08/06/hask-is-not-a-category/)
Wasn't that corrected already? I mean categorical definition of Hask?
If it was, I would like to see the link
For me.. It's a very useful mental model for thinking about architecture & logic
Examples? I haven't really seen many applications of CT, even though I looked for them since I find the idea of CT interesting
You have a function that does A() and another function that does B().
Upon careful inspection or after just writing/using them 10,000s of times[1] you realize they are both special cases of one general function f()[2]. Congrats, you're likely doing CT now, but barely scratching the surface, though.
Let's say you find a way to do a function factory that generates explicit instances of f() -> A() and f() -> B() at runtime for your different use cases as they are needed. You do this 100 times, 1,000 times[1] with many different functions, in many different contexts. You eventually realize that if all your functions and their signatures had the same structure[3] it would be quite easy to mix some (or all?) of them with each other, allowing you to handle a perhaps infinite amount of complexity in a way that's very clean to conceptualize and visualize. Isn't this just FP? Yes, they're very intimately related.
By this point you're 99.9999% doing CT now, but remember to shower regularly, touch grass etc.
CT formalized these structures with mathematical language, and it turns out that this line of thinking is very useful in many fields like ours (CS), Math, Physics, etc.
1. Which is what happened to me.
2. Which sometimes is a way more elegant and simple solution.
3. This term is fundamental and has way more meaning than what I could write here and what one would think on a first approach to it.
Building an abstraction to pull out common logic does not require category theory.
Why not simply use UML?
UML doesn't give ideas for how to actually structure things. Category theory is primarily a theory of nice ways things can be put together or form relationships while maintaining invariants.
Very different thing.
CT is more of a way to abstract all mathematics.
A lot of us don't get it and want to know what we're missing :)
Lets software designers use fancy words and ask for a raise.