5 ms·

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 th

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.
    - wholinator2 3y ago
      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
      - consilient 3y ago
        Lenses: https://arxiv.org/pdf/2001.08045.pdf https://arxiv.org/pdf/2001.08045.pdf SDG: https://tildeweb.au.dk/au76680/NMOS.pdf https://tildeweb.au.dk/au76680/NMOS.pdf HoTT (good luck): https://hott.github.io/book/hott-online-1404-g79e6d60.pdf https://hott.github.io/book/hott-online-1404-g79e6d60.pdf
    - catgary 3y ago
      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.
      - consilient 3y ago
        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.
        catgary 3y ago
        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.
kevinventullo 3y ago
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.
- catgary 3y ago
  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.
  - kevinventullo 3y ago
    Fair enough, I agree monads are an interesting way to think about things.

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.
  - wholinator2 3y ago
    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
    - consilient 3y ago
      Lenses: https://arxiv.org/pdf/2001.08045.pdf https://arxiv.org/pdf/2001.08045.pdf SDG: https://tildeweb.au.dk/au76680/NMOS.pdf https://tildeweb.au.dk/au76680/NMOS.pdf HoTT (good luck): https://hott.github.io/book/hott-online-1404-g79e6d60.pdf https://hott.github.io/book/hott-online-1404-g79e6d60.pdf
  - catgary 3y ago
    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.
    - consilient 3y ago
      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.
      - catgary 3y ago
        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.

kevinventullo 3y ago

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.

catgary 3y ago
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.
- kevinventullo 3y ago
  Fair enough, I agree monads are an interesting way to think about things.