Polynomial Functors: A Mathematical Theory of Interaction [pdf]
topos.site
topos.site
I watched the associated talk[1], and David mentions that Poly is "applicable to database migrations".
Okay, how exactly? What practical problems can I solve with it? Can anyone demonstrate Poly being used somehow for a 1000-table database migration more elegantly than could be achieved using other methods? Is there an O(n^2) or O(exp(n)) scaling lurking in there somewhere, or is this the magic sauce we've all been looking for?
Looking in from the outside, I get the distinct impression that category theorists tend to turn up, simply name things that other people have spent their lives working on, call it "understood", and walk away as-if they've just explained everything that needs to be known about the topic they've merely labelled. They seem like the bug-collectors of mathematics. Okay fine, you've got an impressive collection of bugs, but have you understood evolution well enough from that to help industry with increasing pesticide resistance? Yes? No?
A lot of category theory (at least the more basic parts thereof) is about bringing together concepts that were isolatedly worked on in very different mathematical communities and formulate them in a unified way so that one can see a unifying pattern that was hardly visible before.
> What practical problems can I solve with it?
If you simply want to work on some topic/problem of your interest, category theory will likely be of limited help (except perhaps for finding a more elegant formulation of the things that you work on). If, on the other hand, you seek deep relationships between topics that to most people look unrelated, getting deeply into category theory is likely not a bad idea.
Thus: "from the perspective of someone who is interested in solving practical problem", category theory gives you rather little new problem solving techniques by itself. But category theory gives you a cool lookout to perhaps enable you to apply solution techniques from other areas, where without category theory you would not be able to see the relationship between the technique from a seemingly unrelated area and your problem.
Well, yes, obviously. My analogy is just that: it's like bug collection, bringing together a bunch of samples from many fields into a single museum.
My criticism, I think, is still valid. Just because you've renamed things in a bunch of fields with a consistently obtuse verbiage doesn't mean you've understood anything, or improved any of the fields in a material way. There's a lot of promise, but little delivery.
Category theory is the string theory of mathematics. There. I said it.
I raised a similar critique here before, asking for practical examples from computer science where CT has made a contribution, and someone linked to a CT explanation of automatic differentiation (popularised due to AI).
The thing is, AD predated CT substantially, and was well-understood for a long time. The original theoretical description of AD is something I understood, and the CT description of it was impenetrable, and not useful.
Category theory is something I've always wanted to succeed. It feels like we're on the cusp of something great, like formalising every part of programming languages and compilers for provably correct transformations and optimisations. That would be amazing, but every time I dig into the promise of CT all I see is some hand-wavy "it's applicable to field X" with literally zero further discussion, examples, or practice.
There’s a famous book called Categories for the Working Mathematician. Maybe someday there will be a book called Categories for the Working Programmer.
I like that you call it the string theory of math. It’s a more modern way of saying “abstract nonsense”.
The sociological analogy is a decent one - they're both ambitious sub-fields of little interest to the average practitioner, with a handful of committed opponents and a wildly overgrown internet hatedom - but their positions in their respective disciplines aren't remotely similar.
String theory is a physical theory like any other: pick a spacetime, fill it with dynamical objects, impose some symmetries, and away you go. Category theory, at its most ambitious, wants to be a setting for doing ordinary mathematics in: it belongs in the same general grouping as set theory and higher order logic, not calculus or linear algebra.
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
In CS, abstractions like monads and effect handlers come from category theory. Plotkin and Power did a lot of super technical work on syntax/semantics adjunctions while sorting out the foundations of effect handlers.
In mathematics, category theory is a success story; just have a look at the revolutionary reformulation of algebraic geometry be Alexander Grothendieck and his descendents.
Whether category theory is useful to you in computer science depends a lot on the things that you work on and your "taste in programming style":
If you want to develop new even-higher-level abstractions that unify handling of very different concepts in a unified way, it is in my opinion a great idea to have category theory at your disposal - at least as a source of inspiration, and plausibly for more. Similarly, category theory might be helpful if you want to generalize some cool solution technique to a much larger (and seemingly unrelated!) class of problems.
On the other hand, I can easily find problems in computer science where at least I cannot see how category theory might help me with them (at least with my limited intelligence; I am no Grothendieck ;-) ).
It's unification, not renaming. As a somewhat tortured analogy, consider two concepts: "games", and "mass". Particular concrete games are prior to "games" in general: we learn nothing about chess or basketball by noting that we happen to have a label broad enough to include both, and the worldview of an alien visitor accustomed to thinking only in terms of board-games or ball-games but never simply games is simply different, not incomplete.
But if someone has concepts for mass-of-people and mass-of-planets but doesn't realize that they're all instances of a more general notion of mass-of-things, the situation is different. People-mass and planet-mass are both "mass" not only by convention, as with games, or by brute coincidence, but by physical law. And someone who doesn't know that has a hole in their understanding of physics.
Category-theoretic concepts should be understood in the latter sense. Expecting knowing what a monoid is to deepen your understanding of string concatenation, for instance, is getting things backwards. (This is really an example from abstract algebra, not category theory proper, but the same principle applies). The point is to use your knowledge of string concatenation to get knowledge about {string concatenation | linked lists | regular expressions | MapReduce | max/min | addition | multiplication | convex hulls | ... }, all at once and (once you've paid the upfront cost) all for free.
I was the one who linked that. I wasn't familiar with AD before his talk, but I find it perfectly understandable (modulo Haskell's sometimes foreign-to-me syntax). I think the relevant background here is that I was a math major and had a course in abstract linear algebra (i.e. general vector spaces over fields) and two semesters of abstract algebra (groups, rings, fields) plus dipped my toes in some CT on my own.
He basically notes that D had a slightly nicer chain rule if you write D'f(a)= (f(a), Df(a)) and use D' instead. Then his definition of AD is just the chain rule and the product rule, plus the fact that Df = f for all linear f, applied recursively. So forward mode AD is just writing down facts you learned in calc 1 as a recursive definition (with, I guess, some base cases like sin/cos hard coded).
His description of reverse mode AD is more complicated, but IMO still accessible to someone who's seen dual spaces, product/coproduct vector spaces and maybe enough CT to understand that the map from a vector space to its dual (and matrices to their adjoint) is a contravariant functor.
The basic observation is that he can write the chain rule and product rule as a compositions of linear maps with product/coproduct spaces (which are the same thing for vector spaces). Then he says a biproduct category is one that has (equal) product/coproduct, and notes that the dual map preserves that structure. The point is that biproducts are what he needs to write chain/product rules as compositions of linear maps.
Since he wrote D' recursively in terms of linear maps, and dualizing/taking the adjoint still gives him the structure he needs to do that, he's able to write reverse mode AD as the adjoint representation of D'. He just needs to write the adjoints of the pieces he used, and again compute recursively.
I know at least at my school, the engineering program I was in had a first semester graduate class that dealt some with dual representations (using "test functions" etc. when solving differential equations), so I think it could be distilled down to something appropriate for masters level engineering while retaining the character of what he presented. Like I said, the Haskell syntax was probably the most obscure thing for me.
It's all a matter of perspective and background, but IMO it's sort of like how if you're familiar with linear algebra (including function spaces), then the Fourier transform is just writing a function as a sum of projections onto an orthonormal basis. No need to remember the formulas for it; they're obvious and have simple geometric meaning.
That much I understood myself.
> His description of reverse mode AD is more complicated
And that's where I got lost in the weeds.
I'm sure if I could be bothered, I could sit down for a few weeks or months and gain a working understanding of Category Theory.
My point is not whether I understand or don't understand CT, but... what's the point of spending effort in understanding it?
The CT of forward and reverse mode Automatic Differentiation is cute, but it doesn't seem to have had much practical application in precisely the area where CT ought to be useful.
I mean... both reverse and forward mode AD existed before it was labelled using CT terminology. What did CT add to the SOTA for AD?
So the thing it added is a compact and simple (and therefore pedagogically useful) description of AD for people with the target background.
Goethe wanted to find an underlying pattern common to all plants which would explain how plants grow and develop. Something like a "universal grammar" (to draw an anachronistic parallel to Chomsky) of plants. Goethe called this his "morphological" method and wrote about it in "On the metamorphosis of plants".
One caveat: this paints a slightly too esoteric picture of category theory. Goethe was very idiosyncratic as a scientist, whereas category theory, far from being esoteric, is a common language for all of modern mathematics.
The more basic parts of category theory (which even many mathematicians won't be able to surpass) have in my opinion a slight element of this, even though in my opinion there is still more to even this basic level: getting the categorical perspective often gives you elucidations of various areas of mathematics in the sense that it often shows you how some "side definitions" that are studied in some mathematical area (i.e. definitions that are often mentioned in textbooks, but are not central to the study plan of the textbook) turn out to be more important than it seems without having the framework of category theory at hand.
But after you have reached this level, you can start formulating deep and far-reaching mathematical conjectures using category theory which would be hard to formulate and appreciate without category theory. Here, category theory goes far beyond categorizing things: new categorical abstractions and conjectures formulated in terms of them often become deep new generalizations of topics studied in long-existing mathematical areas.
Just to be clear: this is for mathematics.
For computer science, I rather doubt that if the problems that you are working on are not suitable for formulating in terms of category theory, new definitions that would be hard to formulate without category theory are helpful for the computer science topic that you work on. In this sense: in my opinion most currently existing applications of category theory in computer science are indeed about categorizing things.
If the Broader Impact statements or their equivalents suggest otherwise, well, that's unfortunately how the funding game is played. If you took them at face value you would think all the molecular biologists are curing cancer and every theoretical physics research project is really just a training program. Maybe this reflects poorly on our institutions, but it has nothing to do with the intellectual merit of the work.
And there is a long tradition of category theory being applied to CS theory in PL semantics and type theory. It’s really not a new idea.
I honestly feel bad for some of the students who got swept up into it - I’m not convinced they come out with the hard programming skills of someone working in PL semantics or the flexibility to work in other fields of mathematics that an algebraic topology- or geometry-focused category theory student might have.
The lenses stuff is quite good and I think it would have been well-published/cited in PL theory even without the ACT branding.
I don’t think string diagrams make it any easier to write out an ODE for modeling a physical process.
To reiterate my analogy with String Theory: it has yielded a lot of very useful mathematics... for more String Theories.
In the realm of program design and organization, we find ourselves lacking a comprehensive theory. We lack a framework that determines the most optimal way to compose logic and structure code. To embark on this quest, we must first formally define what it truly means to be "more optimal." While theories for achieving optimal performance exist, we lack a cohesive theory that maximizes modularity, allowing code refactoring to be a seamless process of shifting and recomposing existing modules.
To establish a clear definition of optimality, we require precise and formally defined primitives that symbolize logic. With these foundations in place, we can subsequently develop a formal definition of what constitutes optimal program organization.
Once we have this definition, the next step is calculation. Given these logical primitives, how can we determine the most optimal arrangement of our programs? Calculation becomes possible only when the objective and all the relevant primitives are formalized within a symbolic language.
What lies at the heart of this matter is the potential elimination of the concept of "Design" as we know it. Nobody "Designs" the shortest distance between two points, instead, we calculate the shortest distance between two points with a theory of geometry. This is what I'm talking about: A future where we "calculate the design of programs."
"Design" is merely a label we attach to areas where we lack a formal theory. It represents the wild west of programming, where the absence of an understanding of optimality leads us to rely on haphazard guessing and intuition. This partially explains why the field of IT appears to continuously expand in complexity without ever converging on the perfect technology. Front-end development, in particular, suffers from this uncertainty, as nobody knows for certain if the current status quo is truly superior to previous approaches.
In short: A designer is just someone who makes lots of random guesses. That is the essence of design.
Category Theory, in its current form is mostly impractical. This is not that far from the area that calculus once occupied when it first was discovered. I also cannot definitively claim that category theory will, in the far or near future, provide us with a theory that enables program design through calculation. However, if any theory comes close to achieving this feat, it would undoubtedly be category theory. By formally defining a high-level perspective of logic using only a handful of primitives, it holds the potential to revolutionize our approach by taking the first Required step in developing a formal theory around this topic.
Perhaps it will prove to be futile in the end, or perhaps your reservations will be remembered alongside those who opposed progress throughout history. Recall those who dismissed complex analysis or calculus during their early stages as impractical and useless endeavors. I implore you to exercise patience and observe rather than waste your breath on something you may profoundly misjudge."
To attempt to answer your question, my guess is that no-one has a fully general solution to database migration at the moment. I suspect we aim for good enough and fast enough.
https://youtube.com/playlist?list=PLhgq-BqyZ7i6IjU82EDzCqgER...