15-819 Homotopy Type Theory(cs.cmu.edu)
cs.cmu.edu
15-819 Homotopy Type Theory
http://www.cs.cmu.edu/~rwh/courses/hott/
32 comments
The text was developed open source on GitHub and is available free here: http://homotopytypetheory.org/book/
It's very well done.
What is the significance of Homotopy Type Theory?
It's a foundation of mathematics whose native objects are structures fundamental to higher mathematics (∞-groupoids, which are more or less equivalent to topological spaces up to homotopy), rather than awkward encodings (ZFC "sets", which are tree-like things), and where everything is automatically invariant with respect to abstract notions of equivalence (think isomorphism vs. equality).
The point is that it makes it much more realistic to check complicated math using computers, which will become more important as math inevitably gets more complicated.
Oh, and it happens to be a functional programming language. Which says something about functional programming.
The point is that it makes it much more realistic to check complicated math using computers, which will become more important as math inevitably gets more complicated.
Oh, and it happens to be a functional programming language. Which says something about functional programming.
Well, yes, it's a functional programming language. But not one like most people here are familiar with, so that's a little misleading. It's also an object-oriented language with polymorphism and inheritance.
Specifically, it's (almost exactly) the Calculus of Constructions (http://en.wikipedia.org/wiki/Calculus_of_constructions), the language at the top of the lambda cube (http://en.wikipedia.org/wiki/Lambda_cube).
Specifically, it's (almost exactly) the Calculus of Constructions (http://en.wikipedia.org/wiki/Calculus_of_constructions), the language at the top of the lambda cube (http://en.wikipedia.org/wiki/Lambda_cube).
No, HoTT is not based on the Calculus of Constructions, but instead on intensional Martin-Loef type theory with identity typed. The novel part is the univalence axiom, which MLTT doesn't have.
If you erase types, the underlying programming language is the lambda-calculus, familiar to every programmer.
If you erase types, the underlying programming language is the lambda-calculus, familiar to every programmer.
Yes, Vladimir Voevodsky says HoTT is based on Martin-Loef type theory, but he discovered HoTT by learning the CoC used in Coq, and is implementing his Univalent Foundations library of proofs in Coq. That implies that HoTT is implementable in Coq (with a couple of minor tweaks), which means that CoC is at least as powerful as HoTT. And anyway, according to Voevodsky, they are the same thing.
Really, Martin-Loef type theory is the mathematics foundation, and the Calculus of Constructions is the computer science foundation. HoTT ties them together.
Really, Martin-Loef type theory is the mathematics foundation, and the Calculus of Constructions is the computer science foundation. HoTT ties them together.
It depends on what you mean by "embedding". If one does a deep embedding then powerful calculi can be embedded in much weaker calculi. E.g. Isabelle uses a variant to LF as meta-language to embed all manner of more powerful logics. That doesn't mean LF has a lot of expressive power.
Coq's logic isn't quite the CoC anymore: impredictivity is switched off by default, Coq has universes etc.
With this in mind, I'm not sure what Voevodsky means when he says HoTT and CoC are the same thing.
Coq's logic isn't quite the CoC anymore: impredictivity is switched off by default, Coq has universes etc.
With this in mind, I'm not sure what Voevodsky means when he says HoTT and CoC are the same thing.
I would like to see more clarification of why you'd call HoTT OO. I have no doubt you can encode those things, but I find it strange to try to argue that it doesn't have more in common with the FP tribe than the OO tribe. Given that neither term is terrifically well-defined, I think that's the best you could argue.
Inevitably? Strong words.
Sort of. As t approaches infinity, more and more of the simple parts of math will have been discovered. Therefore the only parts left to discover will be those which are more complicated; hence the overall idea is necessarily correct.
It could instead be the case that all of maths is simple, but that complexity tends to appear whenever we have an incomplete understanding of a domain.
You are misled to believe that mathematics has simple parts and not simple parts, and that simple parts are easier to "discover" than the complex parts.
In fact, the simple parts are usually the most difficult to discover. Why? Precisely because it takes extreme genius to give simple answers to mathematical questions. Over time complicated proofs and definitions get simplified and clarified (such it was with calculus, set theory, logic, group theory, and countless other topics).
So there's no precedent to believe that current mathematics won't be simplified in the future (unless, of course, you believe that all mathematics is complicated; but then you seem to be trying to make an objective point about complexity, so we'll ignore that possibility).
In fact, the simple parts are usually the most difficult to discover. Why? Precisely because it takes extreme genius to give simple answers to mathematical questions. Over time complicated proofs and definitions get simplified and clarified (such it was with calculus, set theory, logic, group theory, and countless other topics).
So there's no precedent to believe that current mathematics won't be simplified in the future (unless, of course, you believe that all mathematics is complicated; but then you seem to be trying to make an objective point about complexity, so we'll ignore that possibility).
This would seem to be true as long as mathematics is discovered rather than invented. Otherwise I beleive that one may be able to invent generalisations that result in a simplification of mathematics.
This assumes that the purpose of math is to prove things, whereas another worthy goal for me at least is enabling humans to truly understand why things are true, and not just what things are true.
No disrespect, but your purpose for math is entirely irrelevant unless you speak for the majority of research mathematicians.
I have a mathematics degree from Harvard, though I haven't taken a poll of research mathematicians. I do think algorithmic theorem proving is a great field of inquiry!
No disrespect, but dkural's idea of what mathematics is about is no more irrelevant than sillysaurus2's or yours, and dkural's view is quite well represented among research mathematicians, first-rate ones included. For a famous example, see William Thurston's "On proof and progress in mathematics" at http://arxiv.org/pdf/math/9404236v1.pdf .
Type Theory is a very foundational way of looking at logic and a very nice functional programming language. It is a strong generalization of, say, Haskell's system. Homotopy TT is a certain kind of TT that introduces a lot of structure to handle notions of equality and identity.
Total layman here, but I thought one of the areas of significance is that a language that uses it can write code that is guaranteed to be bug-free, since the type system is rich enough to be able to prove correctness (given the problem being correctly stated).
That has more to do with type theory directly. So far the lectures have been a great intro to constructive logics which while build to type theory and dependently typed languages, but that's not necessarily the thrust of HoTT.
Bug-free is a bit strong, since you can only use a dependent type-theory like HoTT to establish that a program meets its specification, but the specification might be buggy.
I'm curious what the pre-requisites for this course would be. I don't see it listed anywhere on that page, but I do see intuitionist prepositional logic listed as a topic for classes early in the semester. Other than that, what other topics would help build up a good base for Homotopy Type Theory?
It isn't strictly required, but a background in algebraic topology is really useful for understanding the homotopy bit. That has point-set topology and abstract algebra as pre-reqs. Abstract algebra is a very useful tool for reasoning about computing in its own right.
In addition, experience with proof assistants and dependently typed programming would be really useful.
In addition, experience with proof assistants and dependently typed programming would be really useful.
Dr. Harper suggested that abstract topology isn't such a requirement as they'll develop it synthetically in the class. Then algebraic topology as it's usually developed will become a useful metaphor.
Great response, thank you!
Dr. Harper spends a lot of time developing IPL and it's semantics both as Heyting Algebra and a Bi-Cartesian Closed Category in the first few weeks. I found it easy to follow with a smattering of type theory and category theory background.
I've been wading through the first few weeks of material and have found it incredibly well-paced. Dr. Harper is beginning with the very basics and, though he skips over many supplementary details, is succeeding at slowly introducing new concepts as inevitable given the material presented up until that point. I really recommend the class.
I'm not able to get silverlight + proprietary codecs working on my machine. Is it possible to obtain the video lectures in another format?
The mp4 links are available in the rss feed.
Thanks for pointing that out! It's much easier to pause for jotting down notes, rewind to watch portions of the lecture again, and even speed up portions (between 1.5x and 2.2x is my sweet spot, depending on the presenter) using VLC. As nice as their Silverlight presentation system is, downloadable video files make it much more likely that I will watch all of them, as opposed to only the first few.
It's a shame that the video seems to stutter a lot.
Maybe on later classes they fix that.
Another two pages with worthwhile information on the HoTT book are [1] and [2].
[0] http://existentialtype.wordpress.com/2013/06/22/whats-the-bi...
[1] http://golem.ph.utexas.edu/category/2013/06/the_hott_book.ht...
[2] http://math.andrej.com/2013/06/20/the-hott-book/