3 ms·

> As someone with a maths degree, yet who admittedly hasn't looked into category theory beyond some basic notions, I still don't quite understand why anyone wou

> As someone with a maths degree, yet who admittedly hasn't looked into category theory beyond some basic notions, I still don't quite understand why anyone would want to learn category theory before e.g. abstract algebra Because people think “category theory” means “abstract math” in general, due to cargo-culting in and around the Haskell community.

Karrot_Kream 4y ago
Yeah when I read all of this "category theory expands your mind" thinking, it makes me think that folks were looking for mathematical maturity more than category theory. Work through any good book on algebra and analysis and you'll learn and prove a bunch of stuff about objects and relations.
bmitc 4y ago
I also have a math background but am now a software engineer, and I agree. One can learn category theory all by itself, but it's relatively unimportant in software and computer science as far as I can tell. It's really only powerful as a unifying, abstraction, and conceptual relating tool in upper mathematics where the divisions of mathematics begin to blur.
Tainnor 4y ago
I mean absolutely no disrespect to anyone doing serious work in CT or in Haskell - and I'm actually very interested in Haskell as a language per se and have been exploring it more in recent months - but having spent some time in Haskell communities, I have to agree. There's a lot of empty posturing by people who don't really seem to understand a lot of mathematics but still seem to have very strong convictions about certain aspects of it (constructivism is another such thing).
- btilly 4y ago
  I'm curious why you call out constructivism. I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof." To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system. Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.
  - Tainnor 4y ago
    > I've only really seen constructivism talked about by people who actually have a strong math background. Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it. But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen some NJ Wildberger video where he shittalks the real numbers. So it's not even just constructivism per se, more this mix of unprincipled finitism + constructivism + no axiom of choice (or any mixture thereof), as opposed to anything grounded in some rigorous methodology. Basically the "I don't understand set theory or logic but I've heard that Banach Tarski is weird, so mainstream mathematics must be full of shit". You'd think people wouldn't have hot takes about mathematics, but somehow they do.
    - btilly 4y ago
      I'm glad I haven't seen that then. But conversely it does annoy me to see classical mathematicians dogmatically claim as true statements that depend on their philosophy. And that I have seen a lot of. As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.) But can we agree to both dislike people who argue that 0.999... is not 1?
    - krsrhe 4y ago
    - zozbot234 4y ago
      You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible. And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").

Karrot_Kream 4y ago

Yeah when I read all of this "category theory expands your mind" thinking, it makes me think that folks were looking for mathematical maturity more than category theory. Work through any good book on algebra and analysis and you'll learn and prove a bunch of stuff about objects and relations.

bmitc 4y ago

I also have a math background but am now a software engineer, and I agree. One can learn category theory all by itself, but it's relatively unimportant in software and computer science as far as I can tell. It's really only powerful as a unifying, abstraction, and conceptual relating tool in upper mathematics where the divisions of mathematics begin to blur.

Tainnor 4y ago

I mean absolutely no disrespect to anyone doing serious work in CT or in Haskell - and I'm actually very interested in Haskell as a language per se and have been exploring it more in recent months - but having spent some time in Haskell communities, I have to agree. There's a lot of empty posturing by people who don't really seem to understand a lot of mathematics but still seem to have very strong convictions about certain aspects of it (constructivism is another such thing).

btilly 4y ago
I'm curious why you call out constructivism. I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof." To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system. Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.
- Tainnor 4y ago
  > I've only really seen constructivism talked about by people who actually have a strong math background. Which I don't mind. If you know your maths, your logic and ideally even your philosophy it's perfectly fine to work in constructivism or even prefer it. But I've definitely seen some dumb, uninformed hot takes about how maths is just this big conspiracy that doesn't allow dissenting opinions because they've seen some NJ Wildberger video where he shittalks the real numbers. So it's not even just constructivism per se, more this mix of unprincipled finitism + constructivism + no axiom of choice (or any mixture thereof), as opposed to anything grounded in some rigorous methodology. Basically the "I don't understand set theory or logic but I've heard that Banach Tarski is weird, so mainstream mathematics must be full of shit". You'd think people wouldn't have hot takes about mathematics, but somehow they do.
  - btilly 4y ago
    I'm glad I haven't seen that then. But conversely it does annoy me to see classical mathematicians dogmatically claim as true statements that depend on their philosophy. And that I have seen a lot of. As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.) But can we agree to both dislike people who argue that 0.999... is not 1?
  - krsrhe 4y ago
  - zozbot234 4y ago
    You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible. And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").