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.
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?
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.
> 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."
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.
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...)
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!
I'm happy to hear that you found the first paper interesting!
While I agree that it is unlikely C and Python programmers will take up categorical abstractions any time soon, there is some interest from the JavaScript world. As an example of how this manifests this is a concurrency library (https://www.npmjs.com/package/fluture) and parser combinator library (https://www.npmjs.com/package/parsimmon) that are explicitly using built functors, applicatives and monads as programmatic abstractions. I don't think that this is going to be the mainstream of JavaScript in the near future, but it does suggest that some folks in the JavaScript world think that categorical abstractions are relevant to their practical work.
I also think it is the case that it is a bit strong to claim that Haskell was designed as a programming language for categorical abstractions because none of the ones that I mentioned were included in the initial design of the language. The Haskell 1.0 report[0] was published in 1990 and while it had typeclasses[1], the Functor and Monad typeclasses weren't added until the introduction of monadic IO for Haskell 1.3 in 1996[0]. Moggi's first paper on monads for computation[2] was in 1988, but to my knowledge no one involved in Haskell was introduced to it until several years later[4]. While applicative functors are in the middle of the popular hierarchy, they were the most recently introduced to functional programming. It took until 2008 for them to be explicitly identified as an interesting abstraction in "Applicative programming with effects"[3]. Making a language where programs compose nicely was an explicit design goal, so I don't think that it is a surprise that that's where category theory first landed as an explicit tool for programming abstractions. The categorical abstractions replaced non-categorical abstractions because they did a better job of solving the real problems that the people programming in these languages had, so I think it is a meaningful application of category theory to computing even if it hasn't happened yet in the mainstream of computer programming.
I agree with your assessment of HoTT as well. I'm not currently working on HoTT or on the use of homotopy and (co)homology as programming abstractions, so if they make some contributions to that on the way to their actual goals, I will be super happy.
>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.
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.
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 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!
> 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.
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!
>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.
I know some people have advocated for different terms ('practical foundation of mathematics', 'framework of mathematics') but none of them seem to stick, so linguistic prescriptivism strikes me as a waste of time, especially with how overloaded terminology is in mathematics. Any arising confusion is unfortunate, but as long as it's clear what people mean, I don't see the issue and anyone who actually is able to differentiate between (1) and (2) should be able to understand what is meant from context.
>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.
Sure and if this was the aim of HoTT, dismissing it for this reason would be legitimate, but it's not, as one can see by the reaction of HoTT people to these question: They'll deflect to (2) and do some spiel about 'entrances', because that's what they care about and refer to.
>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.
Then why are there so many people arguing for ZFC as an option for (2)? Not only are there proof assistants based on ZFC and people who advocate for this, a lot of the inane ZFC vs ETCS or HoTT discussions on FOM are absolutely about (2). Hell, even Harvey Friedman has engaged often enough in this e.g. arguing that the ability to make nonsensical statements is actually good because mathematicians start their work by making statements that are often nebulous or wrong.
>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 specifically talking about their views on matters of (2). If your criticism of HoTT is just that they're using the term 'foundation of mathematics' wrong, I'd say the HoTT folks are doing pretty well.
>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.
Are you referring to the development and study of formal systems such as CIC/intuitionistic type theory/HoTT or the actual development of proof assistants that implement these formal systems (Coq, Agda, Lean, etc)? Calling the former engineering seems quite strange to me and I don't see how you could reasonably claim that it's not metamathematics.
>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.
Intuitionism is important for formal verification. For classical reasoning you can just - as you mention - add an axiom, which is also exactly what Lean does. If people dislike HoTT because it's not classical then that's just the fault of bad marketing. It's not indicative of the actual merits of HoTT at all.
>He and his crew have actually formalized a good chunk of real mathematics. That's fairly significant, in my mind.
It's significant and needed work, but there hasn't been any significant news for non-mathematicians. From the point of someone not familiar with mathematics, they've essentially been doing the same thing for about four years.
> Any arising confusion is unfortunate, but as long as it's clear what people mean, I don't see the issue and anyone who actually is able to differentiate between (1) and (2) should be able to understand what is meant from context.
I don't think this is true at all! For example, maybe it is the case that HoTT proponents care solely about (2), and not (1), in which case my criticisms are misguided. But this is not at all the impression I get from reading what they write. Given I'm sensitive to the distinction between (1) and (2), and given I apparently can't infer the difference from context, what are we to conclude? That I just have poor reading comprehensions skills? Maybe so – in which case please help people like me out and use more precise terminology.
OK, I'm being a little coy here, but to be completely serious, I think it's already a confusing enough topic and a bunch of pointless debates could be avoided with better terminology.
> Sure and if this was the aim of HoTT, dismissing it for this reason would be legitimate, but it's not, as one can see by the reaction of HoTT people to these question: They'll deflect to (2) and do some spiel about 'entrances', because that's what they care about and refer to.
I went back to the introduction to the HoTT book [0] to check, to make sure I'm not misremembering things. And they literally say: 'we therefore believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.'
This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1). And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.'
> Then why are there so many people arguing for ZFC as an option for (2)? Not only are there proof assistants based on ZFC and people who advocate for this, a lot of the inane ZFC vs ETCS or HoTT discussions on FOM are absolutely about (2). Hell, even Harvey Friedman has engaged often enough in this e.g. arguing that the ability to make nonsensical statements is actually good because mathematicians start their work by making statements that are often nebulous or wrong.
Yeah, I agree with you. There's no a priori reason to believe ZFC is a good choice for this.
> Are you referring to the development and study of formal systems such as CIC/intuitionistic type theory/HoTT or the actual development of proof assistants that implement these formal systems (Coq, Agda, Lean, etc)? Calling the former engineering seems quite strange to me and I don't see how you could reasonably claim that it's not metamathematics.
Well, metamathematically speaking, the development and study of these formal systems is boring. They don't have anything interesting to say about consistency or provability or whatever, and (as I understand it) they're all mutually intepretable with ZFC (at least the versions used to actually formalize things in practice). So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants.
> It's significant and needed work, but there hasn't been any significant news for non-mathematicians. From the point of someone not familiar with mathematics, they've essentially been doing the same thing for about four years.
I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy. For a long time many people didn't take formalization seriously because it never touched "real" math, and now you're telling me I can do "real" math with it? To the point where undergrads are formalizing the standard undergrad/grad curriculum? That's huge!
>OK, I'm being a little coy here, but to be completely serious, I think it's already a confusing enough topic and a bunch of pointless debates could be avoided with better terminology.
Sure, I just don't think it's going to happen. The HoTT (and category theory) people largely don't care about (1), so they typically don't need to differentiate. More cynically, it's probably also just better marketing, a new 'foundation' certainly sounds more impressive than just a new 'mathematical framework', especially because (1) is generally pretty esoteric.
>This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1).
I don't think so, look at how they actually define 'unformalized mathematics':
"Indeed, many of the proofs described in this book were actually first done in a fully formalized form in a proof assistant, and are only now being “unformalized” for the first time — a reversal of the usual relation between formal and informal mathematics."
The idea is essentially that using HoTT formalisms informally can lead to new insight, which is exactly what part 2 of the book focuses on and they're making it clear that it's about general mathematics rather than metamathematics. If they were talking about (1), you'd expect them to at least do some actual metamathematics with it!
I think your next sentence actually serves to support this further.
>And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.'
And now consider how the sentence actually ends "- and convenient machine implementations, which can serve as a practical aid to the working mathematician". You could argue that it being a practical aid only refers to the convenient machine implementations, but how would 'homootopical content' or 'an "invariant" conception' remotely help with (1)? To me this makes it pretty clear that the aim is to have a practical 'foundation' for the average working mathematician i.e. (2).
>So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants.
Sure, that I don't disagree with, it's definitely in the area of 'applied metamathematics' and there's a reason type theory field is more on the CS side. I just think that you would generally get some pretty strange looks if you called e.g. research on sequent calculus an 'engineering problem', even though it's typically done with the intent of eventually getting a practical system.
>I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy
My point is that often there has been no 'visible' (for a non-mathematician) progress made, so it's curious to me that despite this it still gets posted here every few months. I would have expected some attention if some larger milestone was reached (e.g. formalizing most of an undergrad degree), it's the consistency that is surprising to me.
I think we agree that it's legitimate to motivate HoTT on the grounds of pursuing proof assistants/formalized mathematics, and that other justifications – like competing with ZFC to be a "foundation of mathematics" in the philosophical sense – are not compelling. So whether it's reasonable at all for me take issue with the HoTT hype turns on whether they're offering justifications beyond practically efficient formalization.
I read the introduction to the HoTT book again and it seems to clear to me the justifications offered there go well beyond just better proof assistants. ("Homotopy type theory also brings new ideas into the very foundation of mathematics.") This is also my experience reading HoTT-adjacent people on Twitter (John Baez, random grad students). They clearly have some, I don't know how to put this, fundamentally aesthetic concerns with set theory, and offer various arguments like the ones we agreed were bad.
I appreciate you pointing out that it is possible to make a totally reasonable case for HoTT as a research program that does not resort to such specious arguments. So I am left wondering why so many other people fail to do this.
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.
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.
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)
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)
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).
> I’m not sure whether Lurie realized that it was possible to give rigorous model-independent proofs laying the foundations of infinity category theory. Part of the reason that Dom and I are able to establish something along the lines that I suspect Lurie would have wanted is that we were coming along later. There is also a sociological component to the history. Lurie was forced by the community to choose a specific model to prove theorems about infinity categories, because the ideas were so new, and people didn’t believe the proofs otherwise.
Short version: Even Lurie wasn't ready to generalize from one example :)
Nothing to be ashamed of in any other part of mathematics, I'd say.
> The Mathemagician’s Axiom of Textbook Prerequisites: Let M be the minimum actual prerequisites for an average student being able to read and understand a given presentation of a subject in a mathematics textbook. Let A be the author’s stated prerequisites. Then usually: A <<<<<<< M
> ... My intended audience might be described as peri-graduate students, ranging from advanced mathematics undergraduates, to graduate students, to perhaps even research mathematicians in other disciplines.
I think the prerequisite for "Category Theory in Context" is a grasp of basic category theory ((co-)limits, Yoneda lemma, adjoint functor theorems, etc). You should also have some interest in an abstract maths field that requires all these category theory machinery. So a graduate student in abstract maths sounds about right.
Thanks for the link. I ordered the print book five minutes ago and it will be good to have the PDF also.
I have used Haskell for years, but consider myself a novice at dealing with Monads, etc., while good at writing pure Haskell code. (I wrote a Haskell book, which is free on my website https://markwatson.com/books/).
A few years ago, I randomly had dinner with a math professor who specialized in Category Theory, and it was a very cool conversation. I hope that reading Emily Riehl’s book and listening to some of her teaching videos, that I can grok enough CT to enjoy it.
I think it's fairly misleading to think of impure computation as a core part of the `Monad` abstraction in Haskell[0]. Most of the places I use monads in Haskell are pure e.g. error handling, parsers, working with DSLs. `IO` is where the impurity lives and the monad abstraction just makes it a bit more fun to use, but it isn't essential to the impurity. Haskell had IO before it had monads. I also feel like the emphasis on the Monad abstraction really sells Functor and Applicative short as they are fantastic abstractions in their own right in addition to being important building blocks for the Monad abstraction.
I can really identify with finding Ian Malcolm as inspirational for the positive sides of science. In Jurassic Park the contrast between the do-er scientists (those engineering the dinosaurs) and the think-er scientists (the more abstract theoretical scientist) was pretty starkly and, now that I've been working for a while, correctly portrayed in exposing the motivations those two classes of folks will tend to be working.
If science is a career to acquire cash then it's quite easy to get compromised into focusing on the wrong motivations even if your intentions are quite pure - abstract fields tend to be rather "useless" and thus the same influencing power and money isn't available leading those folks to have a much clearer ability to ethically reason about problems. When you've got co-workers depending on a project going forward to keep a roof over their heads it's a lot easier to compromise morals.
I was once reading a very good Russian book about the Old Church Slavonic language, when it suddenly started praising the glorious achievements of Lenin or something along those lines. It turns out that all books, no matter how unrelated they were in subject matter, were obliged to glorify the Soviet ideology.
You didn't bother to engage with the actual examples she gave, e.g. "It’s also a problem if as an instructor you’re using language that suggests that certain arguments are trivial or that this is something that everybody learned in kindergarten. These are tropes that mathematicians like to use, and I think they’re very alienating to people who, for one reason or other, did not learn about modular arithmetic in kindergarten." - this is, in my experience, a very valid point. It doesn't have to be that way, it's merely correlated with how many mathematicians teach.
I was only responding to the comment (as I explicitly stated below).
Your example doesn’t seem related to politics or feminism at all though. Downplaying the difficulty of everything is just a quirk, one that I personally happen to love. All textbooks have titles like “Elementary X” or “Introductory Y”, no matter how complex. I’ve always found that funny.
Obliged by a authoritarian state (that could be violent, or destroy your career) is incomparable to some peer (that seems not very interested in begin violent nor career destroying) believing others should be obliged. Incomparable. Not sure what logical fallacy this is, but "incomparable" should do the trick.
Why would you want to compare the two, I ask myself?
It’s not quite mandatory to praise feminism yet, for private individuals, but what do you think would happen to the academic career of someone who openly opposed feminism!
Why you want to compare "potential punishment for lack of endorsement of the state" in the USSR with "potential punishment for opposing feminism" in modern days? Those are such different things...
Where I'm from there are plenty of people who oppose parts of feminism. And I dont see them being punished at all. Even I'm openly opposing some of what nowadays is part of feminism!
But the politics she’s talking about have always been in mathematics (and other areas of academia), even if that’s not apparent to people who aren’t negatively impacted by them.
I’ve read countless math textbooks from introductory to PhD level, from a wide timespan, and never once come across any hint of politics. So no, you are simply wrong.
Why is this exclusively limited to textbook content? Is the problematic (for you) quote from a textbook?
If you aren’t comfortable having a discussion about the impact that gender roles and politics have had on women in academia, mathematics in this case, fine. Just say that instead of likening an isolated quote to a cult of personality under an oppressive government.
Take a stab at discussing things in good faith, maybe take the time to try understanding her point, rather than insisting it’s irrelevant.
But that would just be mathematicians tackling issues in their profession, right? If she just means making education more accessible, fairer hiring, etc. that's great, but it's phrased in a pretty 'grand' way that at least to me suggests actions that just aren't really in the ballpark of mathematicians.
Naive understanding of statistics has been repeatedly used to spin data on immigrants (usually with the correlation is not causation fallacy). Real bad ass mathematicians with degrees and cool research positions could way in.
I would not go as far as saying they're obliged, but I'm no mathematician!
For applied mathematicians - especially in statistics - I could see that (though I'd assume social scientists would likely be a better fit - I imagine that an informed take would require more than just pure stats knowledge), but what are pure mathematicians like her going to do?
> I think there’s more stigma attached to femininity in mathematics than femaleness necessarily. As a semi-androgynous queer woman, I think that I kind of fit in in the mathematics community better than I would if I were a cis, straight female.
For anyone who would like to read more on the subject, I'd recommend the works of Julia Serano. She's written extensively about how feminine women are mistreated in academia, even by other feminists and queer women; her most prominent book is Whipping Girl: A Transsexual Woman on Sexism and the Scapegoating of Femininity, but she also has a number of other books and essays on the subject. She's also coined the term "femmephobia" to refer to the phenomenon.
My sister-in-law went through an odd ostracization when trying to get tenure in academia. She and my brother had decided to have children while she pursued her tenure and she ended up getting a lot of friction out of older women in the department who had been forced, when they entered academia, to make a hard choice between being a mother and being a professor.
There are a lot of really strange social dynamics that women can get hit by in the workplace and that one was certainly new to me.
I never seem to get CT or what other people get from it. If you told me there is such a thing as geometric algebra where you have a language to talk about multidimensional spaces and that to solve certain practical problems it worth the effort to ask the question if there might be a space where the answer to that problem is trivial.
CT on the other had always struck me as a long list of if expressions with if expressions inside at infinitum.
Definitely a great article and the math part was incredibly interesting.
At the same time, I had a bit of a nagging fear by this line -
> As a semi-androgynous queer woman, I think that I kind of fit in in the mathematics community better than I would if I were a cis, straight female. I think it also means I’m less likely to get hit on, which is a horrible thing that has happened to a lot of young women in fields where there aren’t enough women.
Obviously without defining "hit on", I do not want to draw too many conclusions. But as a guy, it makes me quite scared that just asking a someone out for a coffee (which I do to people regardless of gender / sex), might get construed as "hitting on" and a horrible thing. All due respect to the people who have been subjected to sexually predatory behavior though. Would like to hear others opinion on the same.
This is a generic tangent veering into outright offtopicness. We try to avoid generic tangents in HN threads because such discussions are more or less all the same, and replacing an interesting specific discussion with a repetitive generic one is a bad trade.
That goes 10x when the topic is an ideological one. It's clear you weren't starting an ideological flamewar on purpose but that's what generic ideological tangents lead to.
The best way to avoid this is to stay grounded in the specifics of the article, especially the ones which have the richest diffs from past repetitive discussion.
I think there’s a saying, “when in doubt, don’t” or something like that, but seriously
As a guy I kind of get where you’re coming from. Sort of. I think being “scared” is a bit much (or can at least be portrayed as the “wrong” connotation to those that care). The way I’d phrase this is, “I want to respect people’s boundaries and certain situations can be trickier to navigate than others and I’d rather not mess it up.”
You can’t account for how someone else will perceive your actions/intentions. In fact, they could probably vary (ie what if someone is looking to be hit on on Tuesday but not Wednesday? What if a person thinks “everyone hits on them”).
For me, I try to treat everyone with respect. Maybe I want to talk more about something, but the other person doesn’t—I’m aware this could be the case so I always try to leave/create/make space for them (ie always provide a way out of the convo for the other person).
I also try to ask myself if “grabbing a coffee” over some conversation is necessary. Interesting people have a ton of people wanting to grab coffee, so maybe a group thing would be better. I also try to consider the persons time (male or female); of course I’d love to steal some time from them or make a professional connection, but you can’t always get what you want.
Just asking if they’d like to go for a coffee and a chat is not intrinsically “hitting on” someone. Obviously tone and context can change everything, but there is no need to be paranoid in general.
For better or worse, any type of interaction (professional or not) is occasionally used as a side channel for romantic interests, and so risks getting misinterpreted as one. Cyber-optimist hopes that online dating platforms will pull this ever-present shadow out of everyday socialization, or at least de-mine the workplace, have proven futile; enough people want the ambiguity. The only reasonable option is to grow a thicker skin and learn saying no and laughing it off.
I've thought on this a lot in the past and the only thing I have hope of addressing it is making any sort of personal/professional relationship spill overs societally verbotten. When folks are at work they intend to work and making any assumption against that line is just going to lead to pain. I really like the team I work with, but I don't ever want them to mix with the group I socialize with solely due to the fact that while at work I want to work.
You want to avoid even social (not just romantical) mixing?
Sorry, but I don't think this is viable with the workers I know (including myself). It is in head-on contradiction with the "do what you love" maxim that most people in my generation are trying to follow. We aren't robots and we don't want to live two completely disjoint lives (or, rather, when we do, we have internet forums, video games and what not for that). In order to have a job where I could completely dissociate from my coworkers, I'd need to find a second skill at which I'm good enough to find employment yet don't care enough about to let it bleed into my life. People are struggling enough with building one skill...
There is probably some good middle ground to be found (how far should my job be from my interests to avoid crossing the streams too much yet allow me to keep it? how much should I let my colleagues into my life?), but no one seems to have invested much in finding it.
There are some people who lean this way and that's fine - there's nothing wrong with it - but there are other people who don't. This will tend to follow an age distinction (with older folks being less interested in having more personal/professional crossover) but I strongly disagree with it being generational.
Your team at work will change over time and new people will join and leave, as you are forced to reconcile changes of employment with the destruction of your social circle I think you'll find that it's easier to move to keeping the two separate. Having children and a strong life partner can also contribute to this - there are a lot of relationships you care deeply about outside of the workplace and you don't want your time at work to be complicated by drama from the fact that you don't value your relationships with your coworker over that of your partner.
Social events at work can be fun and build a stronger team, but viewing your coworkers as your primary social circle probably isn't a healthy long term choice since at some point that relationship will be severed (hope that you don't have to fire a bestie) and someone will be left in an emotional lurch without a shoulder to cry on. I've found it quite helpful to be able to empathize with coworkers and chat about what's going on with work bits in a more safe environment but going into work hoping to find good relationships (social or romantic) is placing a large burden on those you're working with and can end pretty terribly.
I'd also point out that strong social bonds are a reciprocal thing and that while you may be entering the workplace hoping to form those bonds your coworkers may not and the visible existence of cliques in work that exclude some employees that may simply be uninterested in such social activity can lead just as easily to drama in the workplace.
I agree, in the context of the article it means something more sinister than just coffee. But regardless, does not leave me with some fear. Thanks for your reply!
I'm not sure of your point. You're scared of being seen as a predator while women are scared of being preyed upon? So wouldn't you want to try and make spaces as safe as possible so that women wouldn't have to be afraid?
>I think it also means I’m less likely to get hit on, which is a horrible thing that has happened to a lot of young women in fields where there aren’t enough women
Do you think my framing is inaccurate given what she said? How would you describe the negative association with being hit on in the quote above?
>Translating "hit on" as "prey on" might be a sign that you have an unhealthy view of human relationships.
Seeing someone cute at a wedding and making a pass is a far cry from what's been happening in academia for decades where power dynamics are often obvious. There's a reason why very few people would have a problem being (tastefully) hit on in a social situation and why people complain about it happening in a professional situation.
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.