[morty_s]

I love category theory. I found out about it through Haskell and as it turns out it is a branch of mathematics that I feel I’ve been missing my whole life.

Since taking an interest I’ve worked through a couple books on the topic and have listened to a ton of talks/interviews Emily Riehl has given (as well as others).

I really enjoyed her talk at lambda world, “A categorical view of computational effects” (both the content and audio/video quality of this talk are very good!)

Stoked to see this article on HN! I can’t tell if category theory is becoming more popular or if I’m just living in a algorithmically curated/tailored world.

[tkgally]

I had a brush with category theory more than forty years ago. I got a master’s degree in math at the University of Chicago in 1980, Saunders Mac Lane was on the faculty, a few grad students were doing category theory, and I worked through part of Mac Lane’s Categories for the Working Mathematician on my own. I left mathematics soon after—with some regret—and haven’t kept up with the field. The interview with Emily Riehl and the introduction (which I read just now) to her book Category Theory in Context suggest that the field has made a lot of advances in the years since.

I have a question for people who are familiar with recent developments. Forty years ago, the opinions of other math grad students about category theory were divided. Some thought it had the potential to yield great breakthroughs and solve previously unsolved problems in many branches of mathematics. Others thought it was pretty and useful for identifying similar structures in different fields but wasn’t much use for making significant new mathematical discoveries. A sentence in Emily Riehl’s book—“The category-theoretic perspective can function as a simplifying abstraction, isolating propositions that hold for formal reasons from those whose proofs require techniques particular to a given mathematical discipline”—seems to align with the latter opinion.

What has in fact happened in recent decades? Has category theory turned out to be mainly a “simplifying abstraction” as well as an interesting branch of mathematics in its own right? Or has it been used to prove meaty new results in other fields as well?

[bopbeepboop]

I’m not familiar with category theory in depth, but homotopy type theory uses category theory for its semantic model and HoTT’s a big deal in the automated reasoning world.

> Others thought it was pretty and useful for identifying similar structures in different fields but wasn’t much use for making significant new mathematical discoveries. A sentence in Emily Riehl’s book—“The category-theoretic perspective can function as a simplifying abstraction, isolating propositions that hold for formal reasons from those whose proofs require techniques particular to a given mathematical discipline”—seems to align with the latter opinion.

Two points:

1. Being able to “lift and shift” techniques is a big deal in mathematics — so the two cases are the same. A lot of recent innovations are along those lines, where techniques in one area were applied to a new area. In that sense, category theory is wonderful because it gives us a map for how to move techniques around. You could even go so far as to say the algebra-geometry correspondence is category theory’s first “big win”, as it came about as a way to formalize that body of work.

2. Category theory is the native language of data fusion, while categorical syntax is easy to represent in an image-completion kind of way... so category theory is useful for labs working on using machine learning to fuse data and extract semantically meaningful information. Or labs working on an AI model which can suggest improvements to itself.

[spekcular]

> 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/.

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 [1]: https://en.wikipedia.org/wiki/Geometric_Langlands_correspond...

[chas]

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]

"Successfully applied" in what way?

[chas]

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...)

- 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-tr... For way more, see 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)

- 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). 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_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-recursio...). There is a ton more on The Comonad.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 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/CategoricalMani...)

[spekcular]

Thanks. I ask that question a lot on here and I think your first bullet point is the first really substantive answer I've gotten. It's an interesting paper.

I don't have time to read the rest of your links, unfortunately. However, I'm uncomfortable appealing to Haskell (or Ocaml/Scala) as evidence that category theory provides core abstractions for programming. It's true in this context, but only because Haskell was designed to make it true. I am skeptical that category theory has much to say about practical work in the languages used by most programmers, like C, javascript, and python.

Anyway, about HoTT: I don't think it aims to accomplish what you want it to. Its primary concerns seem to be 1) formalized math and 2) serving as an alternative foundation to ZFC. But if it eventually does what you want, great!

[ImprobableTruth]

>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]

> 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-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_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-fa...). And HoTT gets something like 10x more attention than Lean does on HN. So I think "meme" is an apt description.

[ImprobableTruth]

The FOM folk are in general incredibly bearish on proof assistants, so of course they don't care. If you only care about an 'ultimate' foundation that is the best fit to evaluate other systems, rather than a foundation that is amenable to actively working with it, of course you have no reason to care about HoTT.

If you share their opinion, alright, but I personally find this incredibly myopic.

>People definitely say this. See, for instance: 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_u....

I haven't read through all comments, but as far as I see people are actually just criticizing that the encoding is always relevant - that is, they can't talk about objects without encodings, but they don't actually care about the theorems regarding the encoding itself. I think this is fundamentally different from saying 'set theory proves 4 is an element of pi' because otherwise you could levy the same criticism against type theory! After all, there's nothing preventing people from encoding the natural numbers as sets in type theory. The benefit of type theory is that instead you can talk about objects without regard for the encoding which isn't possible with ZFC.

>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. >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.

I guess it matters on how you view it exactly. Under your view you can't state it, but this comes at the cost of not being able to make any at all statements about objects rather than just specific encodings! I'd wager that the vast majority of people would be unsatisfied with this for actively doing mathematics. When people want to talk about the natural numbers, they don't actually care about the specific encoding, they just want to talk about the objects.

The way I see it, if I want to talk about the objects 4 and pi in set theory, I have to consider an arbitrary set that encodes it. Now, because these are still just sets, I can state '4 is an element of pi', but not prove it, because whether it's actually true depends on the specific encoding. This isn't great either, but I think this is a lot closer to how people actually work.

>If my concern is studying the foundations of mathematics, I have not seen a reason why I ought to prefer HoTT over ZFC.

When studying foundations itself ZFC is king, but no one is contesting that. Even HoTT fanatics will admit that its complexity makes it less amenable for certain situations.

>If my concern is formalizing mathematics, Lean seems to be doing a much better job

I'm not sure I understand. So you _do_ accept intuitionistic type theory as a valid alternative to ZFC when one actually wants to formalize mathematics?

Then your dislike of HoTT is even more confounding to me. HoTT is just an extension of intuitionistic type theory. If there's a mature HoTT implementation that stands the test of time (e.g. potentially a fully fleshed out version of cubical type theory), Lean is almost certainly going to incorporate it. Univalence is very much part of 'natural' reasoning, if I show a property for one encoding, I want to be able to transfer that to any other encoding. There's even already an experimental library for Lean that allows you to use univalence. It's just that generally Lean is a lot more conservative rather than experimental. They're not doing a better job because their theoretical foundation is better - it's simply that Kevin Buzzard and his troop is actually putting in the work of doing a lot of formalization.

>And HoTT gets something like 10x more attention than Lean does on HN.

Because HoTT is actually experimental research that could be a breakthrough for intuitionistic type theory, whereas Lean is 'just' people formalizing existing mathematics. I'm actually rather surprised that Kevin Buzzard's work is so popular here - he's certainly doing great work, but there hasn't really been any significant news for the past years. Not only that, but HN isn't a mathematics forum - his work seems about as popular as Coq and Agda here, even though the latter have a far more material impact on software engineering. HoTT is uncharacteristically popular as well, but at the very least there's a chance that it could change the face of formal verification!

[spekcular]

> The FOM folk are in general incredibly bearish on proof assistants, so of course they don't care. If you only care about an 'ultimate' foundation that is the best fit to evaluate other systems, rather than a foundation that is amenable to actively working with it, of course you have no reason to care about HoTT.

> If you share their opinion, alright, but I personally find this incredibly myopic.

I want to distinguish between two senses of "foundation of mathematics":

1) An ontologically minimal language to formalize mathematical reasoning and facilitate proving things about (in)consistency, provability, and relative theory strength, and generally doing metamathematics.

2) A language to actually carry out the details of formalizing mathematics, perhaps jointly by humans and computers, in the sense of the Xena Project and proof assistants.

Here is a claim which might annoy you, but really ought to be uncontroversial: the correct meaning of the term "foundation of mathematics" is the first one. This is what it has meant for about a hundred years, at least, and what someone working professionally in the reverse mathematics/set theory/model theory/logic communities will understand the phrase to mean if you use it in conversation with them.

Now, given this, and given you agree that ZFC does a better job at function (1) above, I think this explains why the FOM people (and more generally those in the communities I listed) find it strange when HoTT is suggested as a "foundation of mathematics." (I can't speak to their opinions on proof assistants, though.) You can see this quite explicitly when Harvey Friedman starts asking questions of the HoTT people; he always asks something about ontological parsimony, remarks how simple the ZFC axioms are (and tells a story about explaining them to his barber, or whatever), and remarks how homotopy is much too sophisticated a concept to be truly foundational.

Moreover, they are going to regard any criticism that ZFC is deficient because it's a poor choice for function (2) as totally besides the point. That's akin to arguing that Turing machines are a poor choice for the foundations of computational theory because it's hard to program them in practice. The same response to applies to your second point about how type theory is "closer to how people actually work"; this was never a figure of merit in the first place.

So, I indeed share this view, but I don't think it's myopic. I think it follows immediately from what a "foundation of mathematics" is.

> I'm not sure I understand. So you _do_ accept intuitionistic type theory as a valid alternative to ZFC when one actually wants to formalize mathematics?

Yes, with the caveat noted below. The practical formalization of mathematics is an engineering problem, not properly speaking one of foundations, as discussed above. This is not to say it's not a deep and interesting problem, just that the difficulties there are mostly orthogonal to those encountered when doing, e.g. metamathematics. One ought to do whatever makes formalization easiest for practitioners.

> Because HoTT is actually experimental research that could be a breakthrough for intuitionistic type theory

This is not compelling to me because I think intuitionism is boring and misguided. I think the majority of practicing mathematicians feel the same way. Of course, you can just add axioms to make it classical, but I'd wager the emphasis on intuitionism is another thing that turns people off from HoTT.

> I'm actually rather surprised that Kevin Buzzard's work is so popular here - he's certainly doing great work, but there hasn't really been any significant news for the past years.

He and his crew have actually formalized a good chunk of real mathematics. That's fairly significant, in my mind.

(You have probably already read this, but in case someone reading this post doesn't know what I mean: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....)

Also, given that it's an engineering problem, there are going to be a bunch of difficulties that only pop up once you start playing with it. So the fact that a group of people have started playing with it, and found some of these problems, and iterated Lean in response – that's good!

[tkgally]

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.

[andi999]

I would also like to know. At least here 20 years ago the opinion was: nice, general framework, but (naturally) no hard theorems.

[jamiek88]

What was the number one thing about category theory that changed your perspective if you don’t mind me asking? You seem very enthusiastic and I’d like to share that enthusiasm one day.

[type_enthusiast]

For me, it was realizing that category theory is the mathematical language of abstraction – almost literally the "principle of least power" in math – and those abstractions often connect to programming abstractions. Even if you're not using words like "Functor" or "Monad" to describe them!

And it can be useful to think of them more abstractly than they actually are, even if you're not going to use them that way (or even talk about them that way in your code). Just making some "ridiculously abstract" connections can help provide a missing piece of architecture, even if you keep the math story to yourself (which you likely should).

So it can (potentially?) be useful to model various things in terms of what they mean "at the most abstract level", and then find ways to capture chunks of that into various architectural abstractions that make sense without category theory (kind of like a Karnaugh map, in a sense).

Sorry if that seems like a lot of "purple prose" or self-important... it really isn't. I think it's the same thing that a lot of people mean when they say "I don't use Haskell but learning it made me a better programmer." I don't use abstract algebra, but learning it made me a better programmer (those statements might even be homomorphic, depending on the Haskell involved)

[bopbeepboop]

Not the person you’re asking, but the “aha” moment for me was connecting whiteboard diagrams with type theory.

Whiteboard diagrams work because they’re a categorical diagram related to the semantics of the program I’m trying to write.

In the sense that CT and TT are “equivalent”, your whiteboard diagrams are your program.

[chas]

The first thing that got me really enthusiastic in category theory was seeing the definition of the categorical product in terms of universal properties. It's a very simple, but very different way of defining objects that makes it easy to see the relationships between similar objects in different contexts. For example, multiplication, the cartesian product, least common multiple, logical conjunction (&&), and structs (or record types) in programming are all products in particular categories* and the universal property definition unifies them very nicely. There isn't really enough space here to spell it out in detail, but this[0] is a good explanation. There is also a very natural way to manipulate the definition (categorical duality) to get coproducts which unify things like logical disjunction (||), greatest common divisor, and disjoint union of sets. This extremely unified view is also nice because if you have an unfamiliar mathematical or computational object, but you know that it has a categorical product, you suddenly know a ton about what you can do with it as well as some interesting questions to ask and properties to go looking for.

This genre of abstraction is all over the place in category theory and it gets way more interesting, but seeing products defined like this and how incredibly unifying of an abstraction it is was the first place that I really saw what the categorical perspective brought to the table.

*Cartesian product within the category of sets and functions between them (amounting to multiplication of cardinals, if one just cares about the action on objects), least common multiple within the category of positive integers ordered by divisibility (a partial ordering being just a special kind of category), logical conjunction within the category of truth values (which can be thought of as sets with at most one element), and structs or record types in the category whose objects are the types of your favorite programming language and morphisms are the programs between them. (From Chinjut, last time I brought up categorical products on hn: https://news.ycombinator.com/item?id=8780786)

[0] https://rnhmjoj.github.io/category-theory-for-programmers/sr...

If you'd to see how this applies more directly to programming, work like this is a direct application of the same definitional strategy for abstraction: https://blog.sumtypeofway.com/posts/introduction-to-recursio...

[adamnemecek]

For me it was the idea of adjoint functors which is the central idea of category theory.

I wrote up a bit on it here https://github.com/adamnemecek/adjoint

[divbzero]

> I really enjoyed her talk at lambda world, “A categorical view of computational effects” [1]

[1]: https://www.youtube.com/watch?v=Ssx2_JKpB3U

[blux]

Thank you for your comment. This inspired me to try to take another stab at studying category theory. I'll start with this lecture: https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbm...

Are there any good books you can recommend on the subject?

[omaranto]

What book will suit you depends on your background. If you have a solid background in math, say an undergraduate degree in math, my favorite book is Emily Riehl's Category Theory in Context [1] (the "context" in the title refers to a background in math).

If you don't know that much math, I'd recommend Tom Leinster's Basic Category Theory [2] or Steve Awodey's Category Theory [3] (particularly if you have some background in computer science or programming).

[1] https://math.jhu.edu/~eriehl/context.pdf

[2] https://www.maths.ed.ac.uk/~tl/bct/

[blux]

Thank you for the pointers.

[mauflows]

What are your favorite books on the topic?

[KirillPanov]

Steve Awodey's Category Theory, hands down.

https://www.goodreads.com/book/show/2047855.Category_Theory

It's a mathematics book written by a philosophy professor that is extremely readable for computer scientists. Very CMU, much wow, such deduction.