6 ms·

Polynomial Functors: A Mathematical Theory of Interaction [pdf]

49 points by solomonb 3y ago

jiggawatts 3y ago
I get that Category Theory is literally a highly theory-based branch of Mathematics, but would it kill its adherents to list an actual practical example? 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 https://www.youtube.com/watch?v=Cp5_o2lDqj0
- carterschonwald 3y ago
  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
  - HelloNurse 3y ago
    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".
- aleph_minus_one 3y ago
  > 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.
  - jiggawatts 3y ago
    > 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.
- catgary 3y ago
  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.
  - consilient 3y ago
    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.
    - catgary 3y ago
      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.
      - consilient 3y ago
        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.
- klysm 3y ago
  Naming abstract compositional concepts let’s you attach a piece of code to them and reuse it.
  - jiggawatts 3y ago
    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.
    - klysm 3y ago
      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.
    - wholinator2 3y ago
      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
- formulathree 3y ago
  >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."
- deleted 3y ago
  [deleted]
- emmelaich 3y ago
  Might not answer your question, but David Spivak wrote a paper on database migration. https://math.mit.edu/~dspivak/informatics/FunctorialDataMigration.pdf 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.
wdpk 3y ago
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-BqyZ7i6IjU82EDzCqgERKjjIPlmh https://youtube.com/playlist?list=PLhgq-BqyZ7i6IjU82EDzCqgER...

49 points by solomonb 3y ago

I get that Category Theory is literally a highly theory-based branch of Mathematics, but would it kill its adherents to list an actual practical example? 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 https://www.youtube.com/watch?v=Cp5_o2lDqj0

carterschonwald 3y ago
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
- HelloNurse 3y ago
  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".
aleph_minus_one 3y ago
> 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.
- jiggawatts 3y ago
  > 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.
catgary 3y ago
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.
- consilient 3y ago
  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.
  - catgary 3y ago
    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.
    - consilient 3y ago
      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.
klysm 3y ago
Naming abstract compositional concepts let’s you attach a piece of code to them and reuse it.
- jiggawatts 3y ago
  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.
  - klysm 3y ago
    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.
  - wholinator2 3y ago
    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
formulathree 3y ago
>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."
deleted 3y ago
[deleted]
emmelaich 3y ago
Might not answer your question, but David Spivak wrote a paper on database migration. https://math.mit.edu/~dspivak/informatics/FunctorialDataMigration.pdf 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.

wdpk 3y ago

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-BqyZ7i6IjU82EDzCqgERKjjIPlmh https://youtube.com/playlist?list=PLhgq-BqyZ7i6IjU82EDzCqgER...