7 ms·

> What has in fact happened in recent decades? Has category theory turned out to be mainly a “simplifying abstraction” [...]? In short: yes, with some exceptio

> What has in fact happened in recent decades? Has category theory turned out to be mainly a “simplifying abstraction” [...]? In short: yes, with some exceptions. The majority of mathematicians are working on problems where category theory is of no importance. A quick list of some of the major exceptions I'm aware of: the general cluster of ideas surrounding the Fukaya category, derived categories, and homological mirror symmetry [0]; geometric Langlands [1]; and the bulk of modern algebraic topology (I have in mind homotopy theory especially). It's also incredibly useful, practically speaking, for modern algebraic geometry and number theory, although my impression is that you have to get pretty deep in the weeds before it becomes more than a linguistic convenience. For a taste of the latter, see the discussion at the beginning of the category section of this algebraic geometry text (which is in principle accessible to someone who has taken an undergraduate course in abstract algebra – though I feel in reality a significant amount of mathematical maturity is required): Section 1.1 of http://math.stanford.edu/~vakil/216blog/ http://math.stanford.edu/~vakil/216blog/. Also, it has become somewhat of a meme here to talk about Homotopy Type Theory. I think this is overhyped; the experts in foundations don't seem to think highly of it. Many arguments for its utility or theoretical importance are, in my opinion, misguided – for example, the claim that set theory proves "junk theorems" such as "pi" being an element of "4." [0]: https://en.wikipedia.org/wiki/Homological_mirror_symmetry https://en.wikipedia.org/wiki/Homological_mirror_symmetry [1]: https://en.wikipedia.org/wiki/Geometric_Langlands_correspondence https://en.wikipedia.org/wiki/Geometric_Langlands_correspond...

chas 6y ago
While I'm not an expert in any of this, I'm primarily interested in Homotopy Type Theory (HoTT) because so many tools originally developed for algebraic geometry and algebraic topology have been successfully applied to logic and programming languages (e.g. categories, functors, natural transformations, monads, comonads, topoi) but homology and homotopy--core tools in algebraic geometry and algebraic topology--haven't been investigated to nearly the same degree in logic and computing. So even if HoTT isn't particularly compelling from the standpoint of pure foundations, I'm still excited for the work they are doing exploring these core tools in geometry in the context of logic and programming languages.
- spekcular 6y ago
  "Successfully applied" in what way?
  - chas 6y ago
    Programmer warning: this is the math jargon heavy version, you don't need to know the math jargon to make use of these tools for writing day-to-day programs. There are too many applications for me to do justice in one message and it is a bit messy because all of these are related, but there are roughly three ways that category theory gets applied to computing: - Reasoning about data within computer programs. In "Generating Compiler Optimizations from Proofs" they make a category where the objects are a representation of expressions in programming languages and the morphisms are expression substitutions. They use this to build general proofs of correctness of compiler optimizations (http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen_tate_popl10.pdf http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen...) - Looking at logics (and thus programming languages) as algebraic objects. Objects are propositions, morphisms are proofs that prove one proposition given assumed propositions. Similarly objects are types, morphisms are functions. That in some contexts these are the same thing is the famous (in programming language circles) Curry-Howard-Lambek correspondence. https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... For way more, see https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#Overview https://ncatlab.org/nlab/show/relation+between+type+theory+a... A different version of this is specifying the mathematical meaning of program execution in terms of directed-complete partial orders which are fruitful to think of categorically. I think Category Theory for Computing Science is the most approachable starting place for that perspective (https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf) - As core abstractions for programming. While you can reason about programs and programming languages with categorical tools, you can also use algebraic abstractions within programs. Functors, strong lax monoidal functors (called Applicative Functors in this context), and monads feature prominently in Haskell's standard library. Basic overview is here (https://wiki.haskell.org/Typeclassopedia https://wiki.haskell.org/Typeclassopedia). The default ones that Haskell uses are all defined as endofunctors on Hask (category of Haskell types and functions between them), so they look a bit funky to a mathematician, but there are other libraries with more mathematically-legible categorical tools as well. (Elsewhere in the thread, Iceland_jack linked to a discussion of one of his proposals: https://www.reddit.com/r/haskell/comments/eoo16m/base_category_polymorphic_functor_and_functorof/ https://www.reddit.com/r/haskell/comments/eoo16m/base_catego...) It is also useful to describe data structures as initial F-algebras in order to abstract over the fold/reduce operation (https://blog.sumtypeofway.com/posts/introduction-to-recursion-schemes.html https://blog.sumtypeofway.com/posts/introduction-to-recursio...). There is a ton more on The Comonad.Reader (http://comonad.com/reader/ http://comonad.com/reader/). For an extremely practical application of non-trivial categorical abstractions see: https://kowainik.github.io/posts/2018-09-25-co-log https://kowainik.github.io/posts/2018-09-25-co-log While I am heavy on the Haskell here because that's what I know best, people also use these abstractions in Ocaml, Scala, and other languages with enough functional and type-level infrastructure for them to be ergonomic to explicitly identify and abstract over. Joseph Goguen also did a ton work applying category theory to computation that spans several of the above application types. A Categorical Manifesto is probably a good place to start and he cites a ton of papers in it that are good next steps. (https://cs.fit.edu/~wds/classes/cdc/Readings/CategoricalManifesto.pdf https://cs.fit.edu/~wds/classes/cdc/Readings/CategoricalMani...)
ImprobableTruth 6y ago
>the experts in foundations don't seem to think highly of it. Feel free to name some of these experts. The only thing I've seen is remarks by generally renowned mathematicians such as Terry Tao who have no interest in either foundations or formal verification (which isn't an indictment, its quite removed from mainstream mathematics), so I don't see why anyone would use this to evaluate the merit of HoTT. >Many arguments for its utility or theoretical importance are, in my opinion, misguided – for example, the claim that set theory proves "junk theorems" such as "pi" being an element of "4." What? Either whoever said that has no clue what they're talking about or you are misremembering their argument. No, set theory doesn't allow you to prove that pi is an element of 4 - but it allows you to state it. And this is actually an issue in so far as that when you want to state actually meaningful theorems, you constantly have to make assertions about what an object is actually supposed to be. If you do this in a formalized, machine amenable way you just end up with a form of type theory. And this isn't actually an argument in favor of HoTT, but just some form of (dependent) type theory, all of which essentially run along the lines of 'This makes proof assistants better/easier to use'. I've never heard a legitimate argument for why dependent type theory is overhyped - even hardcore Isabelle folks will have a hard time disputing that dependent type theory has made much more noteworthy recent advancements. The main argument (from the point of general proof engineering) for HoTT is computable univalence i.e. being able to transfer properties along isomorphisms without the computation getting stuck which is a huge deal. Is it a large enough deal that everyone will adopt it? Who knows, it might be that a more 'practical' proof assistant such as Lean, focusing simply on better automation engineering, will win out, but the hype around HoTT is definitely not just a 'meme'. People over hyping category theory doesn't invalidate the actual research being done.
- spekcular 6y ago
  > Feel free to name some of these experts. Harvey Friedman and Steve Simpson have been quite vocal about it on the Foundations of Mathematics mailing list, for example. There are many others. > What? Either whoever said that has no clue what they're talking about or you are misremembering their argument. People definitely say this. See, for instance: https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems https://mathoverflow.net/questions/90820/set-theories-withou.... And note that not just the questioner but also many commenters assent to that claim. See also the paper Set Theory and Structures by Barton and Friedman, starting p. 15: http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_urelements%20%285%29.pdf http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_u.... I will leave it up to you to decide whether they know what they're talking about. > No, set theory doesn't allow you to prove that pi is an element of 4 - but it allows you to state it. And this is actually an issue in so far as that when you want to state actually meaningful theorems, you constantly have to make assertions about what an object is actually supposed to be. If you do this in a formalized, machine amenable way you just end up with a form of type theory. I am not totally sure about the distinction you are trying to draw here. But I reject the claim that, properly understood, ZFC allows you to prove or state such a thing. What ZFC does is allow one to reformulate all mathematical questions as questions about sets. So if I want to ask some question, like is pi^2 rational, then I can define Dedekind cuts, define squaring, and I know its truth value is the same as a certain question about sets of rational numbers. Now, of course pi is not, philosophically speaking, the same as the set used to encode it. (And in fact there are many ways to do this encoding.) So one cannot even state questions like "Is 3 a member of pi?" in set theory, because 3 and pi are not sets. On the other hand, it is perfectly legitimate to ask questions like, "Is (the pair of natural numbers representing the number) 3 a member of the Dedekind cut associated with pi?" > The main argument (from the point of general proof engineering) for HoTT is computable univalence i.e. being able to transfer properties along isomorphisms without the computation getting stuck which is a huge deal. If my concern is studying the foundations of mathematics, I have not seen a reason why I ought to prefer HoTT over ZFC. But there are various reason to prefer the second, for instance the fact that at some point sets need to get into the picture anyway to give a satisfactory account (e.g. to define large cardinals to study the relative consistency strength of various theories). If my concern is formalizing mathematics, Lean seems to be doing a much better job (see https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa...). And HoTT gets something like 10x more attention than Lean does on HN. So I think "meme" is an apt description.
tkgally 6y ago
My sincere thanks to you and to the others in this thread for taking the time to respond to my question about the applicability of category theory elsewhere in mathematics. I learned a lot from all of your comments. I will retire in two years, after I turn sixty-five. I’ve started to ask myself if that will be too late for me to try to study pure mathematics again.

chas 6y ago

While I'm not an expert in any of this, I'm primarily interested in Homotopy Type Theory (HoTT) because so many tools originally developed for algebraic geometry and algebraic topology have been successfully applied to logic and programming languages (e.g. categories, functors, natural transformations, monads, comonads, topoi) but homology and homotopy--core tools in algebraic geometry and algebraic topology--haven't been investigated to nearly the same degree in logic and computing. So even if HoTT isn't particularly compelling from the standpoint of pure foundations, I'm still excited for the work they are doing exploring these core tools in geometry in the context of logic and programming languages.

spekcular 6y ago
"Successfully applied" in what way?
- chas 6y ago
  Programmer warning: this is the math jargon heavy version, you don't need to know the math jargon to make use of these tools for writing day-to-day programs. There are too many applications for me to do justice in one message and it is a bit messy because all of these are related, but there are roughly three ways that category theory gets applied to computing: - Reasoning about data within computer programs. In "Generating Compiler Optimizations from Proofs" they make a category where the objects are a representation of expressions in programming languages and the morphisms are expression substitutions. They use this to build general proofs of correctness of compiler optimizations (http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen_tate_popl10.pdf http://cseweb.ucsd.edu/~rtate/publications/proofgen/proofgen...) - Looking at logics (and thus programming languages) as algebraic objects. Objects are propositions, morphisms are proofs that prove one proposition given assumed propositions. Similarly objects are types, morphisms are functions. That in some contexts these are the same thing is the famous (in programming language circles) Curry-Howard-Lambek correspondence. https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... For way more, see https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#Overview https://ncatlab.org/nlab/show/relation+between+type+theory+a... A different version of this is specifying the mathematical meaning of program execution in terms of directed-complete partial orders which are fruitful to think of categorically. I think Category Theory for Computing Science is the most approachable starting place for that perspective (https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf https://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf) - As core abstractions for programming. While you can reason about programs and programming languages with categorical tools, you can also use algebraic abstractions within programs. Functors, strong lax monoidal functors (called Applicative Functors in this context), and monads feature prominently in Haskell's standard library. Basic overview is here (https://wiki.haskell.org/Typeclassopedia https://wiki.haskell.org/Typeclassopedia). The default ones that Haskell uses are all defined as endofunctors on Hask (category of Haskell types and functions between them), so they look a bit funky to a mathematician, but there are other libraries with more mathematically-legible categorical tools as well. (Elsewhere in the thread, Iceland_jack linked to a discussion of one of his proposals: https://www.reddit.com/r/haskell/comments/eoo16m/base_category_polymorphic_functor_and_functorof/ https://www.reddit.com/r/haskell/comments/eoo16m/base_catego...) It is also useful to describe data structures as initial F-algebras in order to abstract over the fold/reduce operation (https://blog.sumtypeofway.com/posts/introduction-to-recursion-schemes.html https://blog.sumtypeofway.com/posts/introduction-to-recursio...). There is a ton more on The Comonad.Reader (http://comonad.com/reader/ http://comonad.com/reader/). For an extremely practical application of non-trivial categorical abstractions see: https://kowainik.github.io/posts/2018-09-25-co-log https://kowainik.github.io/posts/2018-09-25-co-log While I am heavy on the Haskell here because that's what I know best, people also use these abstractions in Ocaml, Scala, and other languages with enough functional and type-level infrastructure for them to be ergonomic to explicitly identify and abstract over. Joseph Goguen also did a ton work applying category theory to computation that spans several of the above application types. A Categorical Manifesto is probably a good place to start and he cites a ton of papers in it that are good next steps. (https://cs.fit.edu/~wds/classes/cdc/Readings/CategoricalManifesto.pdf https://cs.fit.edu/~wds/classes/cdc/Readings/CategoricalMani...)

ImprobableTruth 6y ago

>the experts in foundations don't seem to think highly of it. Feel free to name some of these experts. The only thing I've seen is remarks by generally renowned mathematicians such as Terry Tao who have no interest in either foundations or formal verification (which isn't an indictment, its quite removed from mainstream mathematics), so I don't see why anyone would use this to evaluate the merit of HoTT. >Many arguments for its utility or theoretical importance are, in my opinion, misguided – for example, the claim that set theory proves "junk theorems" such as "pi" being an element of "4." What? Either whoever said that has no clue what they're talking about or you are misremembering their argument. No, set theory doesn't allow you to prove that pi is an element of 4 - but it allows you to state it. And this is actually an issue in so far as that when you want to state actually meaningful theorems, you constantly have to make assertions about what an object is actually supposed to be. If you do this in a formalized, machine amenable way you just end up with a form of type theory. And this isn't actually an argument in favor of HoTT, but just some form of (dependent) type theory, all of which essentially run along the lines of 'This makes proof assistants better/easier to use'. I've never heard a legitimate argument for why dependent type theory is overhyped - even hardcore Isabelle folks will have a hard time disputing that dependent type theory has made much more noteworthy recent advancements. The main argument (from the point of general proof engineering) for HoTT is computable univalence i.e. being able to transfer properties along isomorphisms without the computation getting stuck which is a huge deal. Is it a large enough deal that everyone will adopt it? Who knows, it might be that a more 'practical' proof assistant such as Lean, focusing simply on better automation engineering, will win out, but the hype around HoTT is definitely not just a 'meme'. People over hyping category theory doesn't invalidate the actual research being done.

spekcular 6y ago
> Feel free to name some of these experts. Harvey Friedman and Steve Simpson have been quite vocal about it on the Foundations of Mathematics mailing list, for example. There are many others. > What? Either whoever said that has no clue what they're talking about or you are misremembering their argument. People definitely say this. See, for instance: https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems https://mathoverflow.net/questions/90820/set-theories-withou.... And note that not just the questioner but also many commenters assent to that claim. See also the paper Set Theory and Structures by Barton and Friedman, starting p. 15: http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_urelements%20%285%29.pdf http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_u.... I will leave it up to you to decide whether they know what they're talking about. > No, set theory doesn't allow you to prove that pi is an element of 4 - but it allows you to state it. And this is actually an issue in so far as that when you want to state actually meaningful theorems, you constantly have to make assertions about what an object is actually supposed to be. If you do this in a formalized, machine amenable way you just end up with a form of type theory. I am not totally sure about the distinction you are trying to draw here. But I reject the claim that, properly understood, ZFC allows you to prove or state such a thing. What ZFC does is allow one to reformulate all mathematical questions as questions about sets. So if I want to ask some question, like is pi^2 rational, then I can define Dedekind cuts, define squaring, and I know its truth value is the same as a certain question about sets of rational numbers. Now, of course pi is not, philosophically speaking, the same as the set used to encode it. (And in fact there are many ways to do this encoding.) So one cannot even state questions like "Is 3 a member of pi?" in set theory, because 3 and pi are not sets. On the other hand, it is perfectly legitimate to ask questions like, "Is (the pair of natural numbers representing the number) 3 a member of the Dedekind cut associated with pi?" > The main argument (from the point of general proof engineering) for HoTT is computable univalence i.e. being able to transfer properties along isomorphisms without the computation getting stuck which is a huge deal. If my concern is studying the foundations of mathematics, I have not seen a reason why I ought to prefer HoTT over ZFC. But there are various reason to prefer the second, for instance the fact that at some point sets need to get into the picture anyway to give a satisfactory account (e.g. to define large cardinals to study the relative consistency strength of various theories). If my concern is formalizing mathematics, Lean seems to be doing a much better job (see https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa...). And HoTT gets something like 10x more attention than Lean does on HN. So I think "meme" is an apt description.

tkgally 6y ago

My sincere thanks to you and to the others in this thread for taking the time to respond to my question about the applicability of category theory elsewhere in mathematics. I learned a lot from all of your comments. I will retire in two years, after I turn sixty-five. I’ve started to ask myself if that will be too late for me to try to study pure mathematics again.