6 ms·

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've

by j2kun 3y ago

I'm writing a book [1] about "bona fide" applications of mathematics to practical programming problems, where bona fide is my own personal definition [2]. I've had my eye on claims of applications of category theory for many years, and none of them have quite fit the bill (sorry, John, if you're reading this). When they talk about applications to databases it seems quite unrealistic or lacking in sufficient detail to evaluate. And when I talk to people who are actually on the front lines that try to use category theory to solve some problem, they tell me that it ended up being completely useless. I'm open to having my mind changed. The one application that's come the closest is UMAP, [3] though the last time I checked, a few years ago, the jury was still out on whether the structure it produces in applied contexts like biology is spurious. So what specific applications do you know of category theory to practical problems? For the purpose of this post "application" means used by someone in a production software setting to solve a problem not related to category theory. Someone who doesn't care about category theory should care about the problem being solved. And, to be sure, category theory is fine an dandy in its applications to other areas of math, as a unifying language for homology and whatnot. I'm talking about the kind of claims category theory folks sometimes make like "category theory is ushering in a programming revolution and you need to learn it to stay relevant" [1]: http://pmfpbook.org/ http://pmfpbook.org/ [2]: https://buttondown.email/j2kun/archive/whats-in-production/ https://buttondown.email/j2kun/archive/whats-in-production/ [3]: https://umap-learn.readthedocs.io/en/latest/ https://umap-learn.readthedocs.io/en/latest/

matteocapucci 3y ago
You might want to check the most recent work on epidemiogical modeling. Baez blogs extensively about it.
fithisux 3y ago
I ended up there too. Nice for theoretical work, bad for practical work. Functor is useful though.
jiggawatts 3y ago
> When they talk about applications to databases it seems quite unrealistic I read a paper that claimed that the category of polynomial-like things ("Poly") was somehow useful for database migrations! Without a concrete example, that's just an absurd statement to make. If you don't explicitly connect the dots between SQL schemas and polynomials, then you're just hand-waving. It's the equivalent of: "I have a marvellous proof but alas it is too long to fit into this margin."
- solomonb 3y ago
  here you go: https://arxiv.org/pdf/1009.1166.pdf https://arxiv.org/pdf/1009.1166.pdf
  - jiggawatts 3y ago
    This paper is actually interesting and talks about real-world schemas. I particularly like the concept of distinguishable nulls that define a sane equality operator, unlike the traditional SQL NULL. The paper I was referring to used the category Poly, and literally just stated that Poly could be used for database migrations without elaborating further.
    - matteocapucci 3y ago
      That might be a case of the author be really used to a certain crowd and writing for them. The work by Spivak on databases is well-known in ACT so the connection comes pretty easily. Also, in fairness, is pretty easy to Google your way around that claim.
    - solomonb 3y ago
      I don't know the paper you are talking about but the author of this one (David Spivak) does a ton of research on Polynomial Functors and he has a whole book on them: https://topos.site/poly-book.pdf https://topos.site/poly-book.pdf Poly is an incredibly rich category which can be used to describe a ton of stuff such as finite state machines, neural networks, game interactions, wiring diagrams and dynamical systems more generally. I wouldn't be surprised at all if Poly can describe database migrations.
      - j2kun 3y ago
        > can be used to describe a ton of stuff such as One thing that bothers me about applied category theory is that this (being able to describe stuff) always seems to be sufficient for people to claim it is applied. But if the people doing the applying don't find that framing particularly useful, then to me it does not count.
zmgsabst 3y ago
Developing conceptual maps/diagrams, ubiquitous language, and then implementing such a system is topos theory: We’re starting with categorical maps and then transporting that model into a type theory, while maintaining the semantics. Effective patterns in doing so are “applied category theory”.
- j2kun 3y ago
  OK, so name a concrete, production system that followed this pattern.
  - zmgsabst 3y ago
    Two that I know of, when I worked there: - Amazon Device Econ modeling platform, for econometrics - Amazon Tax calculation platform, for things like VAT But more broadly, that’s how you develop software: you’re theory building. 1. Develop language and rules in that language. 2. Give them semantic meaning in a diagram and set of example cases. 3. Develop a corresponding type theory for that. 4. Implement that synthetic domain theory in a general type theory — eg, a programming language. You don’t have to know that it’s topos theory to do those steps, but each is better when you’re explicit about them — and knowing how to guide the first step to get good results at the last step is definitely applied topos theory.
    - j2kun 3y ago
      Are you implying that the people who worked on those two platforms had no idea what topos theory is (but they were "applying" it nonetheless)? Or that they explicitly modeled their stuff in topos theory, and that improved upon the former way they had been doing it without topos theory? I don't count the former as an application of CT, but I would count the latter. References to primary sources would be appreciated, or feel free to email me at mathintersectprogramming@gmail.com with the name or contact information of someone who directly worked on those systems that I could talk to.
febin 3y ago
Loved your previous book, will the new book "Practical Math for Programmers" will be released this year?
- j2kun 3y ago
  Sorry, but no. I've got too much going on. But I am at ~200 pages of a draft
mjan22640 3y ago
Programming is applied algebra, the choice is not using vs not using, but understanding what you are doing vs being ignorant about it. Relevance is in the eye of the beholder. In typical business the incentive is to have a good enough code ready "yesterday", and it will be thrown away tomorrow, as the code and whatever it does are only a means to generate profit and not a goal in itself, and spending time on making it profound is a waste. Wrt production examples, anything written in haskell used categorical constructs explicitly.
- mjburgess 3y ago
  Programming is also applied physics. But understanding the kinetic forces behind typing is no guide to improved programming. To say that learning a field is useful is to say that knowing these abstractions is useful. Much of Haskell's "category theory" is a reuse of terms. Replace Monoid by Appendable, Monad by Composable, Functor by Runnable, etc. and most programming languages are "category theory". This says little about whether knowing the field of category theory will be useful to programming. Indeed, I think there's a good argument to say Haskell programming is much harmed by it. If its authors hadnt used their knowledge of category theory, but rather named the abstractions in more ordinary terms, the language would be more useful to more people.
  - mejutoco 3y ago
    > If its authors hadnt used their knowledge of category theory, but rather named the abstractions in more ordinary terms, the language would be more useful to more people. The language would be just as useful, but it might _feel_ more approachable. Depending on the terms that replaced those it might be more confusing, or the opposite, than it is now.
  - almostdeadguy 3y ago
    > Replace Monoid by Appendable, Monad by Composable, Functor by Runnable, etc. and most programming languages are "category theory". I'm not sure an "Appendable" Int or IO type, or a "Runnable" / "Composable" List type is any less confusing to Joe Programmer. These descriptions do not articulate the same things implied by the Monoid, Functor, and Monad laws. Some of these aren't even correct (i.e. not all Functors are "Runnable", Monadic types do not necessarily compose directly, just via Kleisli composition). > This says little about whether knowing the field of category theory will be useful to programming. Indeed, I think there's a good argument to say Haskell programming is much harmed by it. > If its authors hadnt used their knowledge of category theory, but rather named the abstractions in more ordinary terms, the language would be more useful to more people. I think this is really the least of Haskell's problems. Mystifying/poorly written monad tutorials and conflation with IO (or confusion about how IO works in the haskell runtime) is more responsible for confusing new programmers than the concept itself. I have no background in mathematics above undergrad calc 2 and I was able to understand them just fine.
tutfbhuf 3y ago
> And when I talk to people who are actually on the front lines that try to use category theory to solve some problem, they tell me that it ended up being completely useless. I'm open to having my mind changed. I aim to provide an example of applied category theory in computer science. Your understanding may differ due to the encompassing time frame, however, I ensure that even the most recent findings can rapidly transform into a practical programming concept. The concept of 'monad' was initially introduced by Roger Godement in 1958, known as the 'standard construction'. The term 'monad' itself came into use later in 1967, credited to Jean Bénabou. The connection between monads and functional programming was first established in 1989 by computer scientist Eugenio Moggi. Moggi implemented monads in semantics to interpret the lambda calculus, a computational model that employs variable binding and substitution for function abstraction and application. The formal incorporation of monads into Haskell occurred in 1992 by Philip Wadler. Since then, monads are increasingly being integrated into mainstream programming languages, including JavaScript. For instance, JavaScript Promises can be viewed as a kind of monad. They encapsulate a value and allow its transformation with the .then method, which can be equated to the 'bind' operation in the realm of monads. Furthermore, a new Promise can be generated from any value using Promise.resolve, an operation analogous to the 'return' operation in monads. Promises have a very practical application and are used in programming by millions of developers every day. The concept of a monad is one example that is well-understood; however, there are numerous other such ideas. One of these is the Functor, often referred to as "mappable" in mainstream programming languages. Research in this field is ongoing, with concepts like applicative functors, introduced by Conor McBride and Ross Paterson in 2008, already gaining popularity in languages such as Haskell.
- j2kun 3y ago
  I understand those concepts well, but I find the casual chain of events questionable, especially when the story is told by category theorists. For example, I was once told by a prominent category theorist that certain aspects of the API design for C++ futures was informed by category theory. When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking. This is what it seems category theorists tend to do: they build a framework, express existing ideas within that framework, and then claim that the existing work is an application of category theory. I think that sort of retcon CAN be done. Many math topics like Fourier Analysis have taken practical results, built a math theory behind it, and then converted the entire field to the theory as standard domain knowledge. But the evidence that category theorists have done this, even in the realm of programming language APIs, seems slim. Even if you agree that the APIs align and the people designing the API know their thing is secretly a monad, still calling that a "success" of category theory is rather weak. By comparison, just because something has addition, units, and inverses, it doesn't mean that group theory is being applied in a meaningful way. The nontrivial results about groups that DO seem to lead to "real" applications are related to the structure of particular groups, as used in cryptography. But I have seen little similar in the way of category theory. Porting concepts from category theory to Haskell is nice, maybe, but it's not clear to me that doing so isn't creating as many problems as its solving (e.g., lenses solve a problem that no other language has, and most Haskell programs seem to me to be completely unreadable by anyone except the author, despite me being no stranger to Haskell).
practal 3y ago
I think the important idea from math for programming, and pretty much everything else, is that of a function that operates on functions. You can build on that important idea in different general ways, for example category theory, or type theory. There is a much simpler way of making this idea the foundation of pretty much everything though, see my report "Logic is Algebra" [1]. I've simplified matters further since then (for example, instead of the somewhat unfamiliar notation (lambda x. D P[x]) you write now lambda(D, x. P[x]) (maybe I should even go as far as just writing "lambda(D, x => P[x])", as that triggers probably even more neurons, especially in programmers). lambda is here nothing special, just another operator you can introduce yourself, much like "forall", "exists", "sum", etc. So category theory is, in my opinion, a pretty complicated framework to think in, pushing a certain view of things, and I think there is a more general, yet simpler framework. And I think that will be of use to everyone doing anything vaguely math related, and that certainly includes programmers. [1] https://arxiv.org/abs/2304.00358 https://arxiv.org/abs/2304.00358 (The above report also includes lots of theory, and looks therefore more complicated than it really is. I am working on something new that leaves out the theory, uses more familiar syntax, and emphasises applications)
nabla9 3y ago
I mostly agree. Category theory is typically 1-2 steps separated from what programmers do. Category theory is useful for thinking about X, X is super useful for modelling and designing Y. X in {Petri net, relational algebra, feedback diagrams, type system, ... } and Y in {communication protocol, database, programming language, ... }
- j2kun 3y ago
  Being 2 steps separated is no problem for me. Can you point to any specific production software systems, for which the author of those systems says they used CT for designing stuff, and that it helped in a meaningful way? The only one I have heard of is UMAP, and it was closer to "plain ol' category theory" rather than Petri nets or any of the stuff the applied CT folks do.
deterministic 3y ago
I completely agree. I have been looking for a long while and I haven’t found any examples where using CT made sense. There seems to be a lot of “look at me I am a mathematician!” usage of CT to obfuscate what is really very simple ideas that could otherwise have been explained much simpler without requiring the reader to know an obscure subset of CT. So your basic idea happens to be a Co-Variant Non-Infinitoid Subspace Category? Seriously who cares?
- j2kun 3y ago
  I would care if, e.g., some prior approaches did it poorly, and the category theory helped clarify it among the engineers who then agreed it was a good way to think about their problem.
catgary 3y ago
It’s a bit tough, on one hand John Baez is a great messenger because he’s such a fantastic communicator. But on the other hand, he’s a pretty horrible spokesperson for ACT because the man did theoretical physics and higher category theory for 30 years and now has decided to do “applied” work. It’s pretty evident in this course, he’s just setting up the frameworks people talk about using but isn’t going for any actual results that demonstrate the claimed application. I don’t think he’s ever actually done any applied work before he decided to revolutionize the field. I once watched John talk down to some sort of research electrical engineer at a conference because his diagrammatic calculus didn’t line up with John’s approach, when anyone with a lick of sense would want to understand why their approach didn’t suffice and how these changes addressed its shortcomings - this person was a subject matter expert and Baez condescended to him about his own field! I think his attitude has, unfortunately, rubbed off on a lot of the people in his orbit.
- j2kun 3y ago
  All "applied category theory" books seem to be like this: they start by talking about how great the applications will be, but then instead of getting to the applications, they never stop developing the category theory for its own sake. A lot of math does similar things, to be fair, but I also don't count those as applied.
  - catgary 3y ago
    So, just to offer a few counterpoints there is Tom Leinster’s work on diversity/entropy [1], where people working in mathematical ecology have been happy with his contributions. I’ve also see the Penn robotics group start to use categorical machinery to nail down concepts like bisimulation of dynamical systems and develop a ‘type theory’ for motion plans that has its semantics in a category of dynamical systems [2]. [1] https://arxiv.org/abs/2012.02113 https://arxiv.org/abs/2012.02113 [2] http://www.tac.mta.ca/tac/volumes/35/45/35-45.pdf http://www.tac.mta.ca/tac/volumes/35/45/35-45.pdf I can’t stress enough that Koditschek group are serious people who are using this stuff because it addresses problems they’ve been grappling with.
    - 3y ago
JHonaker 3y ago
It really depends on what your idea of applied is, but Conal Elliot's work is really interesting. His paper on Compiling to Categories [1] pitches programming language semantics as a cartesian closed category [2] allows for really cool stuff by mapping typical evaluation semantics to alternatives like building a computational graph visualization, a pretty printer, and imbuing the original program with automatic differentiation capabilities purely through the categorical interpretation of the same program. Essentially, if you can formulate a desired output of the program as a cartesian closed category, you can do it quite easily. [1]: http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ [2]: A cartesian category with is a category with an operation that lets you pair things together into a new object and get out the original parts with eliminators. Think construct a tuple and have the ability to get the first and second elements out of the tuple. A cartesian closed category adds in the ability to model (partial) function application to its arguments via "apply, curry, and uncurry." See https://en.wikipedia.org/wiki/Cartesian_closed_category https://en.wikipedia.org/wiki/Cartesian_closed_category
- j2kun 3y ago
  This does not appear to pass the criterion I gave: > used by someone in a production software setting to solve a problem not related to category theory If this stuff or its derivative work is used in production in a mainstream compiler (GHC, perhaps?), then I would see it differently.
  - nextaccountic 3y ago
    there was a startup that used this to compile functional programs into circuits not sure if it went anywhere, but it even included self modifying fpga-like circuits iirc
ndnd 3y ago
Sorry, off-topic: can you recommend some (applied) math books for self study people can read before your book is published? I realize the question is somewhat strange and the answer depends on what people work on. Let's say it is not ML/AI. I've enjoyed e.g. 'Calculus' by G. Simmons and Niven's 'The Mathematics of Choice' even though I didn't apply any of that at work.
- j2kun 3y ago
  I can't say I've read any that I could recommend. I have heard nice things about Princeton Companion to Applied Mathematics (TOC: https://assets.press.princeton.edu/chapters/c10592.pdf https://assets.press.princeton.edu/chapters/c10592.pdf) but I haven't ready it personally, and it seems to be more of a reference text and have less stuff relevant to programming specifically.
lamontcg 3y ago
This paper seems to be pretty applied, but I've only skimmed the intro: https://arxiv.org/pdf/1504.05625.pdf https://arxiv.org/pdf/1504.05625.pdf That starts to make sense to me as a sort of generalized framework for Feynman-diagram-like things. Explains why particle physicists would be drawn to category theory as well. Feels like there's still probably a hell of a lot of dots to connect there though.
umutisik 3y ago
This agrees with my experience when I was a young mathematician looking for math that is useful.

by j2kun 3y ago

matteocapucci 3y ago

You might want to check the most recent work on epidemiogical modeling. Baez blogs extensively about it.

fithisux 3y ago

I ended up there too. Nice for theoretical work, bad for practical work. Functor is useful though.

jiggawatts 3y ago

> When they talk about applications to databases it seems quite unrealistic I read a paper that claimed that the category of polynomial-like things ("Poly") was somehow useful for database migrations! Without a concrete example, that's just an absurd statement to make. If you don't explicitly connect the dots between SQL schemas and polynomials, then you're just hand-waving. It's the equivalent of: "I have a marvellous proof but alas it is too long to fit into this margin."

solomonb 3y ago
here you go: https://arxiv.org/pdf/1009.1166.pdf https://arxiv.org/pdf/1009.1166.pdf
- jiggawatts 3y ago
  This paper is actually interesting and talks about real-world schemas. I particularly like the concept of distinguishable nulls that define a sane equality operator, unlike the traditional SQL NULL. The paper I was referring to used the category Poly, and literally just stated that Poly could be used for database migrations without elaborating further.
  - matteocapucci 3y ago
    That might be a case of the author be really used to a certain crowd and writing for them. The work by Spivak on databases is well-known in ACT so the connection comes pretty easily. Also, in fairness, is pretty easy to Google your way around that claim.
  - solomonb 3y ago
    I don't know the paper you are talking about but the author of this one (David Spivak) does a ton of research on Polynomial Functors and he has a whole book on them: https://topos.site/poly-book.pdf https://topos.site/poly-book.pdf Poly is an incredibly rich category which can be used to describe a ton of stuff such as finite state machines, neural networks, game interactions, wiring diagrams and dynamical systems more generally. I wouldn't be surprised at all if Poly can describe database migrations.
    - j2kun 3y ago
      > can be used to describe a ton of stuff such as One thing that bothers me about applied category theory is that this (being able to describe stuff) always seems to be sufficient for people to claim it is applied. But if the people doing the applying don't find that framing particularly useful, then to me it does not count.

zmgsabst 3y ago

Developing conceptual maps/diagrams, ubiquitous language, and then implementing such a system is topos theory: We’re starting with categorical maps and then transporting that model into a type theory, while maintaining the semantics. Effective patterns in doing so are “applied category theory”.

j2kun 3y ago
OK, so name a concrete, production system that followed this pattern.
- zmgsabst 3y ago
  Two that I know of, when I worked there: - Amazon Device Econ modeling platform, for econometrics - Amazon Tax calculation platform, for things like VAT But more broadly, that’s how you develop software: you’re theory building. 1. Develop language and rules in that language. 2. Give them semantic meaning in a diagram and set of example cases. 3. Develop a corresponding type theory for that. 4. Implement that synthetic domain theory in a general type theory — eg, a programming language. You don’t have to know that it’s topos theory to do those steps, but each is better when you’re explicit about them — and knowing how to guide the first step to get good results at the last step is definitely applied topos theory.
  - j2kun 3y ago
    Are you implying that the people who worked on those two platforms had no idea what topos theory is (but they were "applying" it nonetheless)? Or that they explicitly modeled their stuff in topos theory, and that improved upon the former way they had been doing it without topos theory? I don't count the former as an application of CT, but I would count the latter. References to primary sources would be appreciated, or feel free to email me at mathintersectprogramming@gmail.com with the name or contact information of someone who directly worked on those systems that I could talk to.

febin 3y ago

Loved your previous book, will the new book "Practical Math for Programmers" will be released this year?

j2kun 3y ago
Sorry, but no. I've got too much going on. But I am at ~200 pages of a draft

mjan22640 3y ago

Programming is applied algebra, the choice is not using vs not using, but understanding what you are doing vs being ignorant about it. Relevance is in the eye of the beholder. In typical business the incentive is to have a good enough code ready "yesterday", and it will be thrown away tomorrow, as the code and whatever it does are only a means to generate profit and not a goal in itself, and spending time on making it profound is a waste. Wrt production examples, anything written in haskell used categorical constructs explicitly.

mjburgess 3y ago
Programming is also applied physics. But understanding the kinetic forces behind typing is no guide to improved programming. To say that learning a field is useful is to say that knowing these abstractions is useful. Much of Haskell's "category theory" is a reuse of terms. Replace Monoid by Appendable, Monad by Composable, Functor by Runnable, etc. and most programming languages are "category theory". This says little about whether knowing the field of category theory will be useful to programming. Indeed, I think there's a good argument to say Haskell programming is much harmed by it. If its authors hadnt used their knowledge of category theory, but rather named the abstractions in more ordinary terms, the language would be more useful to more people.
- mejutoco 3y ago
  > If its authors hadnt used their knowledge of category theory, but rather named the abstractions in more ordinary terms, the language would be more useful to more people. The language would be just as useful, but it might _feel_ more approachable. Depending on the terms that replaced those it might be more confusing, or the opposite, than it is now.
- almostdeadguy 3y ago
  > Replace Monoid by Appendable, Monad by Composable, Functor by Runnable, etc. and most programming languages are "category theory". I'm not sure an "Appendable" Int or IO type, or a "Runnable" / "Composable" List type is any less confusing to Joe Programmer. These descriptions do not articulate the same things implied by the Monoid, Functor, and Monad laws. Some of these aren't even correct (i.e. not all Functors are "Runnable", Monadic types do not necessarily compose directly, just via Kleisli composition). > This says little about whether knowing the field of category theory will be useful to programming. Indeed, I think there's a good argument to say Haskell programming is much harmed by it. > If its authors hadnt used their knowledge of category theory, but rather named the abstractions in more ordinary terms, the language would be more useful to more people. I think this is really the least of Haskell's problems. Mystifying/poorly written monad tutorials and conflation with IO (or confusion about how IO works in the haskell runtime) is more responsible for confusing new programmers than the concept itself. I have no background in mathematics above undergrad calc 2 and I was able to understand them just fine.

tutfbhuf 3y ago

> And when I talk to people who are actually on the front lines that try to use category theory to solve some problem, they tell me that it ended up being completely useless. I'm open to having my mind changed. I aim to provide an example of applied category theory in computer science. Your understanding may differ due to the encompassing time frame, however, I ensure that even the most recent findings can rapidly transform into a practical programming concept. The concept of 'monad' was initially introduced by Roger Godement in 1958, known as the 'standard construction'. The term 'monad' itself came into use later in 1967, credited to Jean Bénabou. The connection between monads and functional programming was first established in 1989 by computer scientist Eugenio Moggi. Moggi implemented monads in semantics to interpret the lambda calculus, a computational model that employs variable binding and substitution for function abstraction and application. The formal incorporation of monads into Haskell occurred in 1992 by Philip Wadler. Since then, monads are increasingly being integrated into mainstream programming languages, including JavaScript. For instance, JavaScript Promises can be viewed as a kind of monad. They encapsulate a value and allow its transformation with the .then method, which can be equated to the 'bind' operation in the realm of monads. Furthermore, a new Promise can be generated from any value using Promise.resolve, an operation analogous to the 'return' operation in monads. Promises have a very practical application and are used in programming by millions of developers every day. The concept of a monad is one example that is well-understood; however, there are numerous other such ideas. One of these is the Functor, often referred to as "mappable" in mainstream programming languages. Research in this field is ongoing, with concepts like applicative functors, introduced by Conor McBride and Ross Paterson in 2008, already gaining popularity in languages such as Haskell.

j2kun 3y ago
I understand those concepts well, but I find the casual chain of events questionable, especially when the story is told by category theorists. For example, I was once told by a prominent category theorist that certain aspects of the API design for C++ futures was informed by category theory. When I spoke to the people who actually wrote the RFCs, they said category theory had no part in their thinking. This is what it seems category theorists tend to do: they build a framework, express existing ideas within that framework, and then claim that the existing work is an application of category theory. I think that sort of retcon CAN be done. Many math topics like Fourier Analysis have taken practical results, built a math theory behind it, and then converted the entire field to the theory as standard domain knowledge. But the evidence that category theorists have done this, even in the realm of programming language APIs, seems slim. Even if you agree that the APIs align and the people designing the API know their thing is secretly a monad, still calling that a "success" of category theory is rather weak. By comparison, just because something has addition, units, and inverses, it doesn't mean that group theory is being applied in a meaningful way. The nontrivial results about groups that DO seem to lead to "real" applications are related to the structure of particular groups, as used in cryptography. But I have seen little similar in the way of category theory. Porting concepts from category theory to Haskell is nice, maybe, but it's not clear to me that doing so isn't creating as many problems as its solving (e.g., lenses solve a problem that no other language has, and most Haskell programs seem to me to be completely unreadable by anyone except the author, despite me being no stranger to Haskell).

practal 3y ago

I think the important idea from math for programming, and pretty much everything else, is that of a function that operates on functions. You can build on that important idea in different general ways, for example category theory, or type theory. There is a much simpler way of making this idea the foundation of pretty much everything though, see my report "Logic is Algebra" [1]. I've simplified matters further since then (for example, instead of the somewhat unfamiliar notation (lambda x. D P[x]) you write now lambda(D, x. P[x]) (maybe I should even go as far as just writing "lambda(D, x => P[x])", as that triggers probably even more neurons, especially in programmers). lambda is here nothing special, just another operator you can introduce yourself, much like "forall", "exists", "sum", etc. So category theory is, in my opinion, a pretty complicated framework to think in, pushing a certain view of things, and I think there is a more general, yet simpler framework. And I think that will be of use to everyone doing anything vaguely math related, and that certainly includes programmers. [1] https://arxiv.org/abs/2304.00358 https://arxiv.org/abs/2304.00358 (The above report also includes lots of theory, and looks therefore more complicated than it really is. I am working on something new that leaves out the theory, uses more familiar syntax, and emphasises applications)

nabla9 3y ago

I mostly agree. Category theory is typically 1-2 steps separated from what programmers do. Category theory is useful for thinking about X, X is super useful for modelling and designing Y. X in {Petri net, relational algebra, feedback diagrams, type system, ... } and Y in {communication protocol, database, programming language, ... }

j2kun 3y ago
Being 2 steps separated is no problem for me. Can you point to any specific production software systems, for which the author of those systems says they used CT for designing stuff, and that it helped in a meaningful way? The only one I have heard of is UMAP, and it was closer to "plain ol' category theory" rather than Petri nets or any of the stuff the applied CT folks do.

deterministic 3y ago

I completely agree. I have been looking for a long while and I haven’t found any examples where using CT made sense. There seems to be a lot of “look at me I am a mathematician!” usage of CT to obfuscate what is really very simple ideas that could otherwise have been explained much simpler without requiring the reader to know an obscure subset of CT. So your basic idea happens to be a Co-Variant Non-Infinitoid Subspace Category? Seriously who cares?

j2kun 3y ago
I would care if, e.g., some prior approaches did it poorly, and the category theory helped clarify it among the engineers who then agreed it was a good way to think about their problem.

catgary 3y ago

It’s a bit tough, on one hand John Baez is a great messenger because he’s such a fantastic communicator. But on the other hand, he’s a pretty horrible spokesperson for ACT because the man did theoretical physics and higher category theory for 30 years and now has decided to do “applied” work. It’s pretty evident in this course, he’s just setting up the frameworks people talk about using but isn’t going for any actual results that demonstrate the claimed application. I don’t think he’s ever actually done any applied work before he decided to revolutionize the field. I once watched John talk down to some sort of research electrical engineer at a conference because his diagrammatic calculus didn’t line up with John’s approach, when anyone with a lick of sense would want to understand why their approach didn’t suffice and how these changes addressed its shortcomings - this person was a subject matter expert and Baez condescended to him about his own field! I think his attitude has, unfortunately, rubbed off on a lot of the people in his orbit.

j2kun 3y ago
All "applied category theory" books seem to be like this: they start by talking about how great the applications will be, but then instead of getting to the applications, they never stop developing the category theory for its own sake. A lot of math does similar things, to be fair, but I also don't count those as applied.
- catgary 3y ago
  So, just to offer a few counterpoints there is Tom Leinster’s work on diversity/entropy [1], where people working in mathematical ecology have been happy with his contributions. I’ve also see the Penn robotics group start to use categorical machinery to nail down concepts like bisimulation of dynamical systems and develop a ‘type theory’ for motion plans that has its semantics in a category of dynamical systems [2]. [1] https://arxiv.org/abs/2012.02113 https://arxiv.org/abs/2012.02113 [2] http://www.tac.mta.ca/tac/volumes/35/45/35-45.pdf http://www.tac.mta.ca/tac/volumes/35/45/35-45.pdf I can’t stress enough that Koditschek group are serious people who are using this stuff because it addresses problems they’ve been grappling with.
  - 3y ago

JHonaker 3y ago

It really depends on what your idea of applied is, but Conal Elliot's work is really interesting. His paper on Compiling to Categories [1] pitches programming language semantics as a cartesian closed category [2] allows for really cool stuff by mapping typical evaluation semantics to alternatives like building a computational graph visualization, a pretty printer, and imbuing the original program with automatic differentiation capabilities purely through the categorical interpretation of the same program. Essentially, if you can formulate a desired output of the program as a cartesian closed category, you can do it quite easily. [1]: http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ [2]: A cartesian category with is a category with an operation that lets you pair things together into a new object and get out the original parts with eliminators. Think construct a tuple and have the ability to get the first and second elements out of the tuple. A cartesian closed category adds in the ability to model (partial) function application to its arguments via "apply, curry, and uncurry." See https://en.wikipedia.org/wiki/Cartesian_closed_category https://en.wikipedia.org/wiki/Cartesian_closed_category

j2kun 3y ago
This does not appear to pass the criterion I gave: > used by someone in a production software setting to solve a problem not related to category theory If this stuff or its derivative work is used in production in a mainstream compiler (GHC, perhaps?), then I would see it differently.
- nextaccountic 3y ago
  there was a startup that used this to compile functional programs into circuits not sure if it went anywhere, but it even included self modifying fpga-like circuits iirc

ndnd 3y ago

Sorry, off-topic: can you recommend some (applied) math books for self study people can read before your book is published? I realize the question is somewhat strange and the answer depends on what people work on. Let's say it is not ML/AI. I've enjoyed e.g. 'Calculus' by G. Simmons and Niven's 'The Mathematics of Choice' even though I didn't apply any of that at work.

j2kun 3y ago
I can't say I've read any that I could recommend. I have heard nice things about Princeton Companion to Applied Mathematics (TOC: https://assets.press.princeton.edu/chapters/c10592.pdf https://assets.press.princeton.edu/chapters/c10592.pdf) but I haven't ready it personally, and it seems to be more of a reference text and have less stuff relevant to programming specifically.

lamontcg 3y ago

This paper seems to be pretty applied, but I've only skimmed the intro: https://arxiv.org/pdf/1504.05625.pdf https://arxiv.org/pdf/1504.05625.pdf That starts to make sense to me as a sort of generalized framework for Feynman-diagram-like things. Explains why particle physicists would be drawn to category theory as well. Feels like there's still probably a hell of a lot of dots to connect there though.

umutisik 3y ago

This agrees with my experience when I was a young mathematician looking for math that is useful.