[HN Gopher] Homotopy Type Theory [pdf]
___________________________________________________________________
Homotopy Type Theory [pdf]
Author : luu
Score : 44 points
Date : 2020-10-26 23:39 UTC (23 hours ago)
(HTM) web link (hottheory.files.wordpress.com)
(TXT) w3m dump (hottheory.files.wordpress.com)
| remexre wrote:
| Is this an old draft of the book?
| 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 wrote:
| 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-
| fa...
| guerrilla wrote:
| You don't sound like you've heard of the Curry-Howard
| isomorphism. We want practical dependently typed programming
| languages, ZFC is useless for that. Furthermore, LEM is never
| denied, it's just not adopted as an axion and thus requires
| proof per case.
| pgustafs wrote:
| > If all HoTT does is give a theory that's mutually
| interpretable with ZFC, that's not interesting.
|
| "If all python does is give a theory that's mutually
| interpretable with x86 assembly, that's not interesting."
|
| The point is to have better language support for expressing the
| things you want to reason about. I don't find it so far-fetched
| to be interested in better ways of reasoning about equality of
| types (both as a programmer and as a mathematician).
| jcoq wrote:
| There are numerous advantages to having a complete categorical
| or type-theoretic foundations of mathematics, especially one as
| constructive as HoTT. The main advantages in my areas of
| research would be that proofs in "higher-category theory" would
| become less cumbersome. Many set-theoretic proofs in this area
| are non-informative because they are are messy and opaque. This
| is the real promise offered by any alternative theory or
| explanation: insight.
|
| Besides the immediate usefulness: if "all HoTT does is give a
| theory that's mutually interpretable with ZFC", then holy shit
| what an accomplishment!
|
| You seem to have a fundamental misunderstanding about the
| nature of mathematical research. Most fields of research do
| nothing but "give a theory that's mutually interpretable" with
| some other field, or at least did so initially.
| gnulinux wrote:
| What's the point of this comment? It's useful to some people
| therefore people study it. Why assume it needs to be useful to
| all mathematicians?
|
| It is useful for my own work, and thus I study it, why isn't
| this as simple as that?
| da39a3ee wrote:
| What an extraordinary comment. You seem to be missing various
| points:
|
| - Mathematics is a very large field.
|
| - For beginners, it is necessary to have wiser people than
| yourself put up some signposts.
|
| I found the comment you're referring to very illuminating.
| I'm not naively assuming the author's view is the only one,
| or "correct", but s/he certainly like they have some
| familiarity with graduate/research level mathematics in
| relevant areas. So it was very helpful to see, at least from
| the point of view of some mathematicians, that this is not
| considered an important area.
|
| I was left wondering whether the author of that comment
| understood the importance of this stuff in computer science
| (i.e. in academic approaches to programming languages, might
| be the right term, I don't know, I'm pretty ignorant of these
| areas myself), or whether they were only able to criticize it
| from the point of view of pure mathematics.
| voxl wrote:
| Your first point is hysterical considering we as computer
| scientists use many many different programming languages.
|
| Nah the math people are fine with assembly, even though they
| don't actually use it in their work.
| boyobo wrote:
| That's a flawed analogy. Mathematicians do use 'higher level
| languages', that's precisely why most of them don't care
| about HoTT vs set theory. Just like a web dev usually does
| not care about the instruction set of the processor.
| voxl wrote:
| Its not flawed because the correct analogy is: pen and
| paper Turing machines versus Python.
| creata wrote:
| 1. ZFC does everything _you_ need it to do. It 's a really hard
| set of axioms for me to justify compared to MLTT, and it's
| important to me how "obvious" some set of axioms is. MLTT also
| has the advantage that it's very easy to use _without_ encoding
| everything into well-founded, untyped trees, which is nice.
|
| 2. What are these "substantive problems"? I don't have any
| experience in foundations, so I'm genuinely curious.
|
| 3. Sure, intuitionistic mathematics has very little popularity,
| but a lot of that popularity is among computer scientists, for
| fairly obvious reasons.
|
| 4. The HoTT book and the nLab are two of the most out-in-the-
| open developments in math I've seen --- the HoTT book was even
| written in a public GitHub repo iirc. Naturally that has a lot
| of appeal for HN. If you have anything similar (blogs, wikis,
| etc.) for mainstream foundations, I'd love to read them.
|
| 5. Yeah, personally, I'm not really convinced that HoTT is a
| good idea, but I guess we'll just have to wait and see.
| giraj wrote:
| I wouldn't be surprised to see anything related to type-theory
| on here. And I disagree that many people doing HoTT today are
| proposing it as an alternative foundation in anything except
| (categorical) homotopy theory, and I'd like to know where you
| see anyone doing that.
|
| Intuitionism in HoTT isn't about constructivity, which I agree
| is rejected by mainstream mathematicians. It's about the models
| of the theory. For example, LEM doesn't hold in the category of
| bundles over the circle (see my other comment on here). If you
| think of the axiom of choice as "every surjection has a
| section", then this doesn't hold for topological spaces. (Take
| the double cover of the circle; there's no _continuous_
| section.) I disagree that these examples are uninteresting to
| mainstream mathematicians.
| nickdrozd wrote:
| > ...a vehicle for doing mathematics with intuitionistic logic,
| and in particular denying the law of excluded middle...
|
| Intuitionists don't deny the law of excluded middle, they just
| don't admit it as an axiom. From a classical perspective this
| looks like denial, since accepting the law means that you have
| to accept or deny everything, but from an intuitionistic
| perspective that kind of reasoning looks like begging the
| question.
| throwawaygh wrote:
| _> I find it strange that HoTT and HoTT-adjacent stuff gets
| posted here so often._
|
| I don't have any dog in this fight, but I also find it super
| interesting that this topic gets to the 1st page so often.
|
| TBH I think answering that question is more interesting that
| litigating foundations.
| s17n wrote:
| 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-
| mur...)? Idk.
| ajkjk wrote:
| I think people are excited about the connection to type theory
| (tangentially connected to tech) as well as the idea that this
| field and the book are being developed in such an open-source
| way.
| andrewla wrote:
| > 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.
| boyobo wrote:
| You don't need anything like HoTT to start using multi-letter
| variable names.
|
| E.g. https://mitpress.mit.edu/books/functional-differential-
| geome...
| remexre wrote:
| I think Cubical Type Theory (derived from HoTT) is a part of
| the future for general-purpose dependently-typed programming --
| it has canonicity, which I'd argue is necessary for a general-
| purpose programming language, and it being suitable for a
| foundation of mathematics nigh-guarantees it's powerful enough
| to express whatever properties are useful in the domain.
| harveywi wrote:
| So you're saying that cubical type theory will be a good fit
| for cubical programming?
| macromagnon wrote:
| 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.
| AnthonBerg wrote:
| Suggestion: Don't follow advice _not_ to read something.
| ojnabieoot wrote:
| 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/
|
| [2] Available for free here (1 MB pdf)
| https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard....
|
| [3] https://www.manning.com/books/type-driven-development-
| with-i...
| da39a3ee wrote:
| 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 wrote:
| 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/ 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-
| 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 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 wrote:
| Seconded, but it might be worth learning a language with
| algebraic data types first (such as Haskell or OCaml).
| pgustafs wrote:
| 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
|
| (Monoids are the simplest examples of categories)
| platz wrote:
| 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.
| giraj wrote:
| 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
|
| (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.
___________________________________________________________________
(page generated 2020-10-27 23:00 UTC)