15-819 Homotopy Type Theory

http://www.cs.cmu.edu/~rwh/courses/hott/

by mikevm • 13 years ago

79 32 13 years ago

cs.cmu.edu

3rd3• 13 years ago

What is the significance of Homotopy Type Theory?

tel6• 13 years ago

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.

szany• 13 years ago

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.

j2kun2• 13 years ago

Inevitably? Strong words.

nardi2• 13 years ago

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

tunesmith• 13 years ago

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

tel6• 13 years ago

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.

mafribe3• 13 years ago

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.

jds375• 13 years ago

The text was developed open source on GitHub and is available free here: http://homotopytypetheory.org/book/ It's very well done.

siddboots2• 13 years ago

I'm not able to get silverlight + proprietary codecs working on my machine. Is it possible to obtain the video lectures in another format?

namarkiv• 13 years ago

The mp4 links are available in the rss feed.

dmunoz2• 13 years ago

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.

tel6• 13 years ago

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.

ddellacosta2• 13 years ago

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?

chas• 13 years ago

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.

ddellacosta2• 13 years ago

Great response, thank you!

tel6• 13 years ago

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.

tel6• 13 years ago

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.

dmunoz2• 13 years ago

The linked course pages contains a good synopsis, but Robert Harper's own blog post "What’s the big deal with HoTT?" [0] gives a wider view about its motivation and history.

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/

15-819 Homotopy Type Theory

Related Stories