Polynomial Functors: A Mathematical Theory of Interaction [pdf](topos.site)
topos.site
Polynomial Functors: A Mathematical Theory of Interaction [pdf]
https://topos.site/poly-book.pdf
37 comments
> category theorists tend to turn up, simply name things that other people have spent their lives working on
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.
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.
> about bringing together concepts
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.
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.
> Category theory is something I've always wanted to succeed.
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 ;-) ).
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 ;-) ).
> 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
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.
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 mean, the modern language of algebraic geometry and homotopy theory is based on advanced category theory. David Spivak, the author of this book, wrote a great thesis on cobordisms and used categorical techniques to sidestep hard problems in intersection theory. You can also look at some of Ezra Getzler’s work to see how setting up clean categorical abstractions can make it easier to attack hard problems in geometry.
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 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.
I get the complaint. In the old days people would sometimes say “abstract nonsense” when talking about category theory related topics. It’s increasingly an important part of a basic mathematical education at the graduate level. Eventually there may be a spillover into other areas like computer science where so called practical uses occur. But maybe not. It’s still too early to say.
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”.
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”.
> 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.
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.
There's this, but the programmer doesn't have to be working:
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
https://github.com/hmemcpy/milewski-ctfp-pdf
https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
https://github.com/hmemcpy/milewski-ctfp-pdf
Since you provide a zoological metaphor, let me offer an alternative. Category theory is much more like Goethe's work on the /Urpflanze/ (primeval plant). Linné had developed a way of systematically naming species of plants, but Goethe was not satisfied by this approach.
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.
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 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.
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.
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.
> 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.
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?
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?
If you already understand AD, maybe there's not much point for you. The point may be for others that have some background in linear algebra and maybe rings/modules (so they've seen a few non-contrived examples of categories and functors), and who haven't encountered AD. For them, Conal's description is concise and memorable. Again, it's like describing Fourier transforms as an orthogonal decomposition: for someone who hasn't studied linear algebra, functions being "infinite dimensional vectors" will sound scary, and eyes will glaze over. They might prefer to stick to just working at the level of manipulating integrals and using "clever tricks". For those with more linear algebra background, a bunch of the basic theorems around Fourier transforms become immediate, and you don't need to think about them. The "tricks" turn out to be geometrically motivated.
So the thing it added is a compact and simple (and therefore pedagogically useful) description of AD for people with the target background.
So the thing it added is a compact and simple (and therefore pedagogically useful) description of AD for people with the target background.
So would it be fair to say that category theorists are mostly concerned with categorizing things?
> So would it be fair to say that category theorists are mostly concerned with categorizing things?
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.
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.
So, this is a tough thing to say publicly because I really respect a lot of David’s early work on derived differential geometry - please don’t judge category theory as a field based on Applied Category Theory™. To quote a random tweet, Applied Category Theory is the cryptocurrency of the sciences. They’ve managed to convince some senior Air Force or Navy person that translating well understood mathematics to string diagrams will make scientists more productive because they won’t need to code, and are thus getting lots of funding.
This is pretty uncharitable. Applied category theorists aren't really part of "applied math" in the conventional sense (numerical linear algebra, HPC, operations research, and so on) and they're not trying to be. The thing they're applying category theory to is CS theory.
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.
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.
I must have sat through a dozen of talks about how double push-out rewriting theory is going to revolutionize mathematical biology/linguistics/etc. I can give firsthand evidence that it’s not limited to funding proposals.
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.
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.
Sure, I'm not saying there's no hype. And DPO rewriting has gone the way of all concurrent systems stuff, I agree. But good work that's hyped up as an era-defining breakthrough is ... still good work. Lenses are great. Synthetic differential geometry is imo super promising. HoTT is going to make for a beautiful failed dream. None of it is the Principia, but it shouldn't have to be. And there's plenty of space between there and crypto scams.
You list many highly interesting sounding theories. As someone who's just entering post undergraduate academia, do you suggest any resources for learning a survey of the field currently? I'd heard of category theory and thought it was awesome but in all my looking I've never seen the number of current in development and actually applied ideas you've listed here. Thanks
I think you’re conflating criticism of Applied Category Theory™ with criticism of category theory.
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.
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.
Maybe so. I'm not sure what the TM means, at any rate. But to my mind there's a clear distinction between the sort of stuff John Baez does, which could reasonably be called "applied", and the sort of stuff Jacob Lurie does, which absolutely is not. And there's good and valuable work in both clusters.
Maybe! I just think I was exactly the sort of industrial scientist who would be the market for something like CatLab.jl, or a lot of papers that intersected with my new-found industrial domain, and I just never found anything compelling. I feel like I wasted a fair bit of time trying to get anything out of it, so I’ve been left pretty skeptical of anything coming of California or Oxford.
The lenses stuff is quite good and I think it would have been well-published/cited in PL theory even without the ACT branding.
The lenses stuff is quite good and I think it would have been well-published/cited in PL theory even without the ACT branding.
As a former pure mathematician turned software dev, I couldn’t agree more. The language and ideas of Category Theory are indispensable for doing modern algebraic number theory, but I have yet to see a compelling example of Category Theory applied to software development.
I think things like monads and linear/affine types have their place, and I actually quite like lenses in functional languages (even Jax uses them in disguise to safely modify arrays in-place).
I don’t think string diagrams make it any easier to write out an ODE for modeling a physical process.
I don’t think string diagrams make it any easier to write out an ODE for modeling a physical process.
Fair enough, I agree monads are an interesting way to think about things.
Might not answer your question, but David Spivak wrote a paper on database migration. https://math.mit.edu/~dspivak/informatics/FunctorialDataMigr...
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.
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.
Naming abstract compositional concepts let’s you attach a piece of code to them and reuse it.
The problem is that many CT proponents have stated this, but not provided anything other than toy examples, or Haskell libraries that nobody uses outside of the CT crowd.
To reiterate my analogy with String Theory: it has yielded a lot of very useful mathematics... for more String Theories.
To reiterate my analogy with String Theory: it has yielded a lot of very useful mathematics... for more String Theories.
Apologies if you're an expert because i am certainly not, but i was under the impression that parts of the string theory mathematique had started to become useful in other endeavors. Things like a second derivation of general Relativity from first principles, or just generally an immense set of mathematical tricks for renormalization and such that are being applied even to current field theories. I do understand the political zeitgeist around string theory is that it's not useful and never will be, but I've heard murmuring recently that while 10 dimensions isn't collapsing easily to 3 or 4, the techniques learned during the exploration are actually highly useful in varied area of high level theoretical physics. Namely the much more physical models built on QFT rather than string theory
In scala I’ve productively used monad, semigroup etc because the type system was barely good enough to express it. In other languages i haven’t had as much implementing the concepts because of poor type systems.
The table of contents sounds like it’s borrowing from a bunch of Haskell libraries I’ve used, but without clarifying why the tools help to engineer complex systems
In Haskell, CT-based subtle type distinctions and CT-based cleverly leveraged automatic proofs are the only available advanced tools that help to engineer complex systems; this book seems to belong to the same genre of CT developments, because it discusses all sorts of useful things that turn out to be "polynomials".
>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?
History has shown us that various mathematical concepts, such as imaginary numbers, initially seemed utterly useless upon their invention. Yet, they eventually found profound applications and significance.
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."
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."
[deleted]
I found the book a little bit hard as an entry point to the subject, those lectures were very helpful
https://youtube.com/playlist?list=PLhgq-BqyZ7i6IjU82EDzCqgER...
https://youtube.com/playlist?list=PLhgq-BqyZ7i6IjU82EDzCqgER...
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?
[1] https://www.youtube.com/watch?v=Cp5_o2lDqj0