4 ms·

As a math course, I felt category theory was interesting as a way of unifying ideas across different areas of mathematics. But I never quite seen a value of it

As a math course, I felt category theory was interesting as a way of unifying ideas across different areas of mathematics. But I never quite seen a value of it for programming (but maybe it's just me)

ants_everywhere 2y ago
It's IMO the right setting to talk about logic. That's one of the reasons it unifies ideas in math. Computer science is mostly an application of logic which is why category theory has become a useful tool in theoretical computer science.
- CarpaDorada 2y ago
  If you're talking about toposes, many logics do not correspond to them. It's the other way around: many category theorists/logicians needed jobs and found computer jobs and hence the category theoretic perspective in CS.
  - ants_everywhere 2y ago
    You don't know what you're talking about. Applications of category theory to computer science predate the first US computer science department. There weren't any computer science jobs to speak of. Categorical logic is larger than elementary topoi. I would wager that you can't name a logic not expressible in category theory.
    - CarpaDorada 2y ago
      >Applications of category theory to computer science predate the first US computer science department. This doesn't sound plausible: according to Wikipedia, Eilenberg and Mac Lane introduced concepts of CT in 1942, and CT was originally used mainly homological algebra, with applications in logic/semantics later. Certainly CT was given credence by Grothendieck and Serre, working on (and solving) Weil's conjecture in the 50s and 60s. Lawvere's 1963 thesis predated categorical logic (according to his own words, <http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html> p. 12, "but the method here, and indeed in the whole ensuing categorical logic, is to exploit the uniqueness by using adjointness itself as an axiom"). The first computer science department in the US was started in 1962 in Purdue University. Meanwhile for contrast the proofs of Church and Turing were published in 1936. >I would wager that you can't name a logic not expressible in category theory. I prefaced my statement with an "if"; you're not talking about toposes apparently. The interpretability of one theory in another is a concern of logicians and I'm not familiar with any restrictions on category theory, indeed it can be used for logics. I do not know topos theory but I was basing my statement on what I heard Colin McLarty say in an interview of his <https://www.youtube.com/watch?v=81sPQGIWEfM https://www.youtube.com/watch?v=81sPQGIWEfM>, can't give timestamp; he definitely named logics that cannot be expressed by the topos of a space. I feel that you've used two straw men: 1) specifically naming US 2) ignoring my "if topos" and saying "expressible in CT".
lambdas 2y ago
As primarily an engineer doing maths, with code on the side, I feel the exact same. It’s been way more of use to me in pulling together parts of topology, linear algebra, geometric algebra, homology et al than discovering furtive programming abstractions.

ants_everywhere 2y ago

It's IMO the right setting to talk about logic. That's one of the reasons it unifies ideas in math. Computer science is mostly an application of logic which is why category theory has become a useful tool in theoretical computer science.

CarpaDorada 2y ago
If you're talking about toposes, many logics do not correspond to them. It's the other way around: many category theorists/logicians needed jobs and found computer jobs and hence the category theoretic perspective in CS.
- ants_everywhere 2y ago
  You don't know what you're talking about. Applications of category theory to computer science predate the first US computer science department. There weren't any computer science jobs to speak of. Categorical logic is larger than elementary topoi. I would wager that you can't name a logic not expressible in category theory.
  - CarpaDorada 2y ago
    >Applications of category theory to computer science predate the first US computer science department. This doesn't sound plausible: according to Wikipedia, Eilenberg and Mac Lane introduced concepts of CT in 1942, and CT was originally used mainly homological algebra, with applications in logic/semantics later. Certainly CT was given credence by Grothendieck and Serre, working on (and solving) Weil's conjecture in the 50s and 60s. Lawvere's 1963 thesis predated categorical logic (according to his own words, <http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html> p. 12, "but the method here, and indeed in the whole ensuing categorical logic, is to exploit the uniqueness by using adjointness itself as an axiom"). The first computer science department in the US was started in 1962 in Purdue University. Meanwhile for contrast the proofs of Church and Turing were published in 1936. >I would wager that you can't name a logic not expressible in category theory. I prefaced my statement with an "if"; you're not talking about toposes apparently. The interpretability of one theory in another is a concern of logicians and I'm not familiar with any restrictions on category theory, indeed it can be used for logics. I do not know topos theory but I was basing my statement on what I heard Colin McLarty say in an interview of his <https://www.youtube.com/watch?v=81sPQGIWEfM https://www.youtube.com/watch?v=81sPQGIWEfM>, can't give timestamp; he definitely named logics that cannot be expressed by the topos of a space. I feel that you've used two straw men: 1) specifically naming US 2) ignoring my "if topos" and saying "expressible in CT".

lambdas 2y ago

As primarily an engineer doing maths, with code on the side, I feel the exact same. It’s been way more of use to me in pulling together parts of topology, linear algebra, geometric algebra, homology et al than discovering furtive programming abstractions.