11 ms·

Homotopy Type Theory (2012) [pdf]

108 points by luu 6y ago

macromagnon 6y ago
I've been wanting to go towards category theory, homotopy type theory, etc. but I realized I need more abstract/algebraic geometry and then I need some topology, etc before category theory so I have more examples of morphisms to draw from. Right now I'm mostly studying linear algebra and some combinatorics. Very interested in linear operators and the relationship between differential/finite difference operator, falling/rising factorials, stirling numbers, bernoulli numbers, etc. I'm hoping math will get me a more interesting job than java programmer but I enjoy the math for its own sake anyways.
- platz 6y ago
  I'm afraid homotopy type theory has zero relevance towards anything related to applied programming at this stage, especially if you are not already an academic doing PHD-level research. if you want to learn some functional programming along with abstractions actually used in FP programming, that is one thing, but that is not homotopy type theory, which is squarely in the domain of purely abstract mathematics which would be interesting from a pure mathematics perspective, not a programming perspective. The paper does appear to include some proof that utilize Coq, but unless you're interested in software that checks the validity of mathematical proofs, that is not going to help you get a more interesting programming job.
- ojnabieoot 6y ago
  I would strongly recommend looking at “standard” dependently-typed theories and languages (or even proof assistants without dependent types), instead of trying to plunge into homotopy theory. Learning how dependent types work will be much more illuminating than trying to catch up on the algebraic topology. While the link between topology and formal logic is certainly interesting, I think you’ll be much better served by starting on the logic side of things. Software Foundations is a well-known book / series of Coq programs for theoretical computer science. [1] Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems. Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read and actually enjoyed :) [1] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ [2] Available for free here (1 MB pdf) https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.... [3] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
  - pgustafs 6y ago
    Seconded, but it might be worth learning a language with algebraic data types first (such as Haskell or OCaml).
  - da39a3ee 6y ago
    Thanks for this very helpful comment which I've bookmarked for the links. Could I ask you for any more recommendations?! I have background in standard undergrad math (linear algebra, calculus, real analysis, etc) and some basic undergrad CS, and I work as a software engineer (backend web stuff). However I've never really studied formal logic, or theoretical CS, or formal methods / verification, or type theory, and I was thinking of doing so. I enjoy studying math/theoretical things for its own sake, but I am of course also interested in techniques which might touch upon software engineering in practice. Do you have any opinions on whether I am proposing something at all sensible for myself, and if so what sort of order to take things in? Any recommended sources of exercises to work on (with solutions? seeing as I might well be self-studying) Or lecture courses, or anything available online (even if it costs money) Online communities you'd recommend for asking for help, e.g. with problems encountered in self-study? And any more recommended books/lecture notes of course.
    - ojnabieoot 6y ago
      Disclaimer: I am not a domain expert in type theory and my background is algebraic combinatorics, not computer science. I also hate online courses, don’t like collaborative learning, and tend to read books and papers by myself. So I’m not a great source of advice for most people. Unfortunately I don’t have many more suggestions that would be good pedagogically. Benjamin Pierce (who wrote Software Foundations) has another very famous intro book, Types and Programming Languages: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ which is regarded as a “Bible” of type theory for computer scientists. Note: I haven’t personally read this, but I have read the sequel, Advanced Types and Programming Languages. Both books have exercises and most exercises have solutions. Simon Peyton-Jones wrote a very good book, the Implementation of Functional Programming Languages. It is old (1987), but free, a good read, and covers most of the “important” topics without assuming too much background: https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/ https://www.microsoft.com/en-us/research/publication/the-imp... For formal verification - there are definitely better-qualified people than me. I found a lot of the source code to CompCert C (a verified C compiler) illuminating: https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert However, it will be difficult to understand without doing Software Foundations first (I still find personally tactics-style proofs in Coq confusing and don’t like Coq as much as Idris or Agda). I am very shy and can’t help you with the online communities :) The type theory subreddit is pretty active and they seem nice.
- pgustafs 6y ago
  If you're a programmer, I wouldn't worry too much about examples of morphisms from math (unless you're interested in the math for its own sake). You already know tons of morphisms -- every function in any programming language is a morphism (e.g. square x = x * x is a morphism Num -> Num). By the way, if you're interested in categories, you might like this post about using monoids for GPU parsing: https://raphlinus.github.io/gpu/2020/09/05/stack-monoid.html https://raphlinus.github.io/gpu/2020/09/05/stack-monoid.html (Monoids are the simplest examples of categories)
- AnthonBerg 6y ago
  Suggestion: Don't follow advice not to read something.
remexre 6y ago
Is this an old draft of the book? http://saunders.phil.cmu.edu/book/hott-online.pdf http://saunders.phil.cmu.edu/book/hott-online.pdf EDIT: Should've read the first page, whoops; still, the book provides a lot more material, so if you're interested, give it a read next.
spekcular 6y ago
I find it strange that HoTT and HoTT-adjacent stuff gets posted here so often. Even in the world of pure mathematics, this is a backwater. As I understand it, the two main selling points are providing a foundation for mathematics and a framework for automated theorem proving, but: 1) We already have a perfectly good foundation of mathematics. It's called ZFC [1], and it does everything we need it to do. If all HoTT does is give a theory that's mutually interpretable with ZFC, that's not interesting (at least to mainstream workers in the foundations of mathematics, who would rather tackle substantive problems). There are also people like Per-Martin Lof who want to use HoTT as a vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle, but at that point you've let the mask slip and you're advocating something that interests approximately zero mainstream mathematicians. 2) It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics. It could be, it couldn't be, but this is ultimately an empirical question . Some comments on the state of the field are given in [2]. [2]: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa...
- s17n 6y ago
  It's popular at CMU? It got a huge-for-pure-math grant 5 years ago (https://homotopytypetheory.org/2014/04/29/hott-awarded-a-muri/ https://homotopytypetheory.org/2014/04/29/hott-awarded-a-mur...)? Idk.
- andrewla 6y ago
  > vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle I think this is the basis for the enthusiasm, almost entirely. There's a growing perception that a lot of mathematical abstractions that are purely naval-gazing have arisen from ZFC, and the intuitionalists and finitists are gaining followers amongst amateur and upcoming mathematicians. I don't have data to back this, just a feeling that I get. And I think in particular this is attractive to programmers because this skews closer to what we've learned about computability and program design, and I think there's even some hope of moving forward from obscure notation and single-letter variable names towards a syntax for doing mathematics that can be more expressive and easier to verify.
giraj 6y ago
For people wanting to learn HoTT, I'd rather recommend Rijke's book assembled from his lectures at CMU: https://github.com/EgbertRijke/HoTT-Intro https://github.com/EgbertRijke/HoTT-Intro (Disclaimer: I'm a mathematician working in HoTT and (higher) category theory.) Like with most advanced concepts in any field, there are lots of misunderstandings pertaining to HoTT. To me, the underlying insight is that the "right" abstract setting for a lot of classical homotopy theory is that of an infinity-topos (whose precise definition is an open question, but we have candidates). Theorems proven in HoTT hold in any infinity-topos, and HoTT is (conjecturally) the internal language of these. For anything outside of homotopy theory, HoTT isn't (immediately) interesting. It's certainly not trying to provide foundations for set-based mathematics, but for (categorical) homotopy theory, sure. Some mathematicians take issue with the logic being intuisionistic; e.g. neither the law of the excluded middle, nor double negation hold in HoTT. This is not about constructivity (which I agree, mainstream mathematicians will reject), but about the spaces being modeled. For example, a mainstream mathematician will say that a space is either empty or has a point. However, in the category of bundles over the circle, points are sections; and so the double cover doesn't have any point, for example. Neither is it empty.
The_rationalist 6y ago
I get it that Homotopy type theory is an alternative to set theory that is based upon topology. What's less clear from their marketing is whether it's just yet another formulation of something equivalent (set/standard type theory/category theory) Or if like any really interesting theory it does lead to different prediction or has properties which make it superior in some ways. Until such marketing is addressed I won't spend brain energy on learning it. As an example, theorem provers are really an interesting topic, I heard that Homotopy type theory was used in some theorem provers but couldn't find whether it leaded to any significant improvements. As an AGI researcher, should I learn Hott?
- Ericson2314 6y ago
  I think the a good place to get a sense of the motivation is https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... / https://ncatlab.org/nlab/show/computational+trinitarianism https://ncatlab.org/nlab/show/computational+trinitarianism Let me break it down even more basically: 1. There's a sense in many corners academia that there's too much new but ephemeral work, and not enough librarian work codifying and polishing existing ideas for more better presentatinon. (See https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-technopastoral/ https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-te... for a good digression on that.) 2. Category theory, and related fields, emerged as a conceptual framework to organize many disparate parts of mathematics into a tighter whole, addressing such concerns (though it predates the modern form of those concerns). Category theory however still came about as "regular" math with pen, paper, thinking, and informal natural language proofs. 3. A bunch of computer scientists studying programming languages become interested in Category Theory and Type Theory. They pretty quickly become the main people perusing both of those fields. They also decide they fit together quite well. (If you are Platonist, this is not surprising as both are very general. If you a Conwayist, this is not surprising because if the same people are interested in two things, either those things will become increasingly intertwined, or if they really are incompatible and the group of people will disaggregate.) 4. Programming language theorists are not content with just a common mental framework for all math, they also want computer-codified proofs and computer-aided workflows. (See https://en.wikipedia.org/wiki/Automath https://en.wikipedia.org/wiki/Automath for the first major attempt.) Type theory, being far more mechanistic/syntactic than category theory, is their obvious go-to. ------ 5. Enter Vladimir Voevodsky. Vladimir Voevodsky is a fields medalist, i.e. a bonafide exceptional mathematician by mainstream standards who can finally lend some legitimacy to the efforts of these mathematician-computer scientists who often raise eyebrows. VV's field specialty is (within) topology, which always had a friendlier relationship with category theory, and so easily picks everything up after an experience with bad proof of his that no one else caught leads him to think formal methods are needed. 6. HoTT was sparked by some insight from VV. The intent is actually 2-fold: both to fix some annoyances with the automated theorem proovers, and to make some progress on advanced topology. It just so happens that the same tricks looked promising for both problems. So HoTT in particular is useful for cutting-edge topology research (that's few of us) or better human computer interaction (that's far more of us). For the latter, just getting on board with Category theory and type theory before the HoTT special sauce is most of the mental work. HoTT is a not big additional step if others are doing the heavy lifting to figure out what it is in the first place. 7. During all of this, the US military decided that cybersecurity is a problem, and that programming language theorists had a compelling story on how to do defense more aggressively than traditional security types. That has injected a bunch of money into this stuff whereas before there was hardly any (by computer scientist standards).

108 points by luu 6y ago

I've been wanting to go towards category theory, homotopy type theory, etc. but I realized I need more abstract/algebraic geometry and then I need some topology, etc before category theory so I have more examples of morphisms to draw from. Right now I'm mostly studying linear algebra and some combinatorics. Very interested in linear operators and the relationship between differential/finite difference operator, falling/rising factorials, stirling numbers, bernoulli numbers, etc. I'm hoping math will get me a more interesting job than java programmer but I enjoy the math for its own sake anyways.

platz 6y ago
I'm afraid homotopy type theory has zero relevance towards anything related to applied programming at this stage, especially if you are not already an academic doing PHD-level research. if you want to learn some functional programming along with abstractions actually used in FP programming, that is one thing, but that is not homotopy type theory, which is squarely in the domain of purely abstract mathematics which would be interesting from a pure mathematics perspective, not a programming perspective. The paper does appear to include some proof that utilize Coq, but unless you're interested in software that checks the validity of mathematical proofs, that is not going to help you get a more interesting programming job.
ojnabieoot 6y ago
I would strongly recommend looking at “standard” dependently-typed theories and languages (or even proof assistants without dependent types), instead of trying to plunge into homotopy theory. Learning how dependent types work will be much more illuminating than trying to catch up on the algebraic topology. While the link between topology and formal logic is certainly interesting, I think you’ll be much better served by starting on the logic side of things. Software Foundations is a well-known book / series of Coq programs for theoretical computer science. [1] Lectures on the Curry-Howard Isomorphism[2] is my favorite (graduate-level) introduction to type theory and the lambda calculus, including the “lambda cube” and pure type systems. Finally, while Type-Driven Development With Idris[3] is not at all “theoretical,” it is still an excellent introduction to dependent types and the idea of proof-as-program. It’s also the only book about a specific programming language I’ve ever read and actually enjoyed :) [1] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ [2] Available for free here (1 MB pdf) https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.... [3] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
- pgustafs 6y ago
  Seconded, but it might be worth learning a language with algebraic data types first (such as Haskell or OCaml).
- da39a3ee 6y ago
  Thanks for this very helpful comment which I've bookmarked for the links. Could I ask you for any more recommendations?! I have background in standard undergrad math (linear algebra, calculus, real analysis, etc) and some basic undergrad CS, and I work as a software engineer (backend web stuff). However I've never really studied formal logic, or theoretical CS, or formal methods / verification, or type theory, and I was thinking of doing so. I enjoy studying math/theoretical things for its own sake, but I am of course also interested in techniques which might touch upon software engineering in practice. Do you have any opinions on whether I am proposing something at all sensible for myself, and if so what sort of order to take things in? Any recommended sources of exercises to work on (with solutions? seeing as I might well be self-studying) Or lecture courses, or anything available online (even if it costs money) Online communities you'd recommend for asking for help, e.g. with problems encountered in self-study? And any more recommended books/lecture notes of course.
  - ojnabieoot 6y ago
    Disclaimer: I am not a domain expert in type theory and my background is algebraic combinatorics, not computer science. I also hate online courses, don’t like collaborative learning, and tend to read books and papers by myself. So I’m not a great source of advice for most people. Unfortunately I don’t have many more suggestions that would be good pedagogically. Benjamin Pierce (who wrote Software Foundations) has another very famous intro book, Types and Programming Languages: https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ which is regarded as a “Bible” of type theory for computer scientists. Note: I haven’t personally read this, but I have read the sequel, Advanced Types and Programming Languages. Both books have exercises and most exercises have solutions. Simon Peyton-Jones wrote a very good book, the Implementation of Functional Programming Languages. It is old (1987), but free, a good read, and covers most of the “important” topics without assuming too much background: https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/ https://www.microsoft.com/en-us/research/publication/the-imp... For formal verification - there are definitely better-qualified people than me. I found a lot of the source code to CompCert C (a verified C compiler) illuminating: https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert However, it will be difficult to understand without doing Software Foundations first (I still find personally tactics-style proofs in Coq confusing and don’t like Coq as much as Idris or Agda). I am very shy and can’t help you with the online communities :) The type theory subreddit is pretty active and they seem nice.
pgustafs 6y ago
If you're a programmer, I wouldn't worry too much about examples of morphisms from math (unless you're interested in the math for its own sake). You already know tons of morphisms -- every function in any programming language is a morphism (e.g. square x = x * x is a morphism Num -> Num). By the way, if you're interested in categories, you might like this post about using monoids for GPU parsing: https://raphlinus.github.io/gpu/2020/09/05/stack-monoid.html https://raphlinus.github.io/gpu/2020/09/05/stack-monoid.html (Monoids are the simplest examples of categories)
AnthonBerg 6y ago
Suggestion: Don't follow advice not to read something.

remexre 6y ago

Is this an old draft of the book? http://saunders.phil.cmu.edu/book/hott-online.pdf http://saunders.phil.cmu.edu/book/hott-online.pdf EDIT: Should've read the first page, whoops; still, the book provides a lot more material, so if you're interested, give it a read next.

spekcular 6y ago

I find it strange that HoTT and HoTT-adjacent stuff gets posted here so often. Even in the world of pure mathematics, this is a backwater. As I understand it, the two main selling points are providing a foundation for mathematics and a framework for automated theorem proving, but: 1) We already have a perfectly good foundation of mathematics. It's called ZFC [1], and it does everything we need it to do. If all HoTT does is give a theory that's mutually interpretable with ZFC, that's not interesting (at least to mainstream workers in the foundations of mathematics, who would rather tackle substantive problems). There are also people like Per-Martin Lof who want to use HoTT as a vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle, but at that point you've let the mask slip and you're advocating something that interests approximately zero mainstream mathematicians. 2) It's not at all clear HoTT, or type theory in general, is the best solution for formalizing mathematics. It could be, it couldn't be, but this is ultimately an empirical question . Some comments on the state of the field are given in [2]. [2]: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa...

s17n 6y ago
It's popular at CMU? It got a huge-for-pure-math grant 5 years ago (https://homotopytypetheory.org/2014/04/29/hott-awarded-a-muri/ https://homotopytypetheory.org/2014/04/29/hott-awarded-a-mur...)? Idk.
andrewla 6y ago
> vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle I think this is the basis for the enthusiasm, almost entirely. There's a growing perception that a lot of mathematical abstractions that are purely naval-gazing have arisen from ZFC, and the intuitionalists and finitists are gaining followers amongst amateur and upcoming mathematicians. I don't have data to back this, just a feeling that I get. And I think in particular this is attractive to programmers because this skews closer to what we've learned about computability and program design, and I think there's even some hope of moving forward from obscure notation and single-letter variable names towards a syntax for doing mathematics that can be more expressive and easier to verify.

giraj 6y ago

For people wanting to learn HoTT, I'd rather recommend Rijke's book assembled from his lectures at CMU: https://github.com/EgbertRijke/HoTT-Intro https://github.com/EgbertRijke/HoTT-Intro (Disclaimer: I'm a mathematician working in HoTT and (higher) category theory.) Like with most advanced concepts in any field, there are lots of misunderstandings pertaining to HoTT. To me, the underlying insight is that the "right" abstract setting for a lot of classical homotopy theory is that of an infinity-topos (whose precise definition is an open question, but we have candidates). Theorems proven in HoTT hold in any infinity-topos, and HoTT is (conjecturally) the internal language of these. For anything outside of homotopy theory, HoTT isn't (immediately) interesting. It's certainly not trying to provide foundations for set-based mathematics, but for (categorical) homotopy theory, sure. Some mathematicians take issue with the logic being intuisionistic; e.g. neither the law of the excluded middle, nor double negation hold in HoTT. This is not about constructivity (which I agree, mainstream mathematicians will reject), but about the spaces being modeled. For example, a mainstream mathematician will say that a space is either empty or has a point. However, in the category of bundles over the circle, points are sections; and so the double cover doesn't have any point, for example. Neither is it empty.

The_rationalist 6y ago

I get it that Homotopy type theory is an alternative to set theory that is based upon topology. What's less clear from their marketing is whether it's just yet another formulation of something equivalent (set/standard type theory/category theory) Or if like any really interesting theory it does lead to different prediction or has properties which make it superior in some ways. Until such marketing is addressed I won't spend brain energy on learning it. As an example, theorem provers are really an interesting topic, I heard that Homotopy type theory was used in some theorem provers but couldn't find whether it leaded to any significant improvements. As an AGI researcher, should I learn Hott?

Ericson2314 6y ago
I think the a good place to get a sense of the motivation is https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/ https://existentialtype.wordpress.com/2011/03/27/the-holy-tr... / https://ncatlab.org/nlab/show/computational+trinitarianism https://ncatlab.org/nlab/show/computational+trinitarianism Let me break it down even more basically: 1. There's a sense in many corners academia that there's too much new but ephemeral work, and not enough librarian work codifying and polishing existing ideas for more better presentatinon. (See https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-technopastoral/ https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-te... for a good digression on that.) 2. Category theory, and related fields, emerged as a conceptual framework to organize many disparate parts of mathematics into a tighter whole, addressing such concerns (though it predates the modern form of those concerns). Category theory however still came about as "regular" math with pen, paper, thinking, and informal natural language proofs. 3. A bunch of computer scientists studying programming languages become interested in Category Theory and Type Theory. They pretty quickly become the main people perusing both of those fields. They also decide they fit together quite well. (If you are Platonist, this is not surprising as both are very general. If you a Conwayist, this is not surprising because if the same people are interested in two things, either those things will become increasingly intertwined, or if they really are incompatible and the group of people will disaggregate.) 4. Programming language theorists are not content with just a common mental framework for all math, they also want computer-codified proofs and computer-aided workflows. (See https://en.wikipedia.org/wiki/Automath https://en.wikipedia.org/wiki/Automath for the first major attempt.) Type theory, being far more mechanistic/syntactic than category theory, is their obvious go-to. ------ 5. Enter Vladimir Voevodsky. Vladimir Voevodsky is a fields medalist, i.e. a bonafide exceptional mathematician by mainstream standards who can finally lend some legitimacy to the efforts of these mathematician-computer scientists who often raise eyebrows. VV's field specialty is (within) topology, which always had a friendlier relationship with category theory, and so easily picks everything up after an experience with bad proof of his that no one else caught leads him to think formal methods are needed. 6. HoTT was sparked by some insight from VV. The intent is actually 2-fold: both to fix some annoyances with the automated theorem proovers, and to make some progress on advanced topology. It just so happens that the same tricks looked promising for both problems. So HoTT in particular is useful for cutting-edge topology research (that's few of us) or better human computer interaction (that's far more of us). For the latter, just getting on board with Category theory and type theory before the HoTT special sauce is most of the mental work. HoTT is a not big additional step if others are doing the heavy lifting to figure out what it is in the first place. 7. During all of this, the US military decided that cybersecurity is a problem, and that programming language theorists had a compelling story on how to do defense more aggressively than traditional security types. That has injected a bunch of money into this stuff whereas before there was hardly any (by computer scientist standards).