Higher-Dimensional Type Theory | Hacker News Reader

Higher-Dimensional Type Theory

existentialtype.wordpress.com

76 pointsfogus10 comments

Every time I read something about type theory I just can't get past the notation. I've taken two classes on it, and somehow it just never stuck. I struggled with it as much in those classes as I do now. Once I parse the statements the ideas always end up coming through as elegant and intuitive, but getting there is a slog. Does anyone else have this problem? Is my brain just broken w.r.t. type theory symbols?

Type theorists must use such strange notation to make sure there's never a collision between something in their meta language, and something that someone would actually use in a language. :)

For the interested, Steve Awodey has an introductory article, with pointers to the relevant literature: http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf

This is the kind of thing I like to see on HN.

A big topic in type theory nowadays is equational reasoning. The classic example is, how can you prove that two functions are observationally equivalent -- that they give the same output for all inputs? Bob discusses that in his book.

More generally, you can discuss various other notions of equivalence, both for functions and (in this case) types. So if we do allow a programmer to define their own notions of equivalence, is that good enough? Not quite -- it can be difficult to propagate this notion through to derivative constructs. You'd like for there to be a way to get all sorts of "free" theorems basically. So I think that is what this blog post is beginning to talk about, in somewhat technical terms.

For a second I was imagining Helvetica in 4D+

Anyone want to explain this using less jargon?

Well, Benjamin Pierce has a 600 page book: http://www.amazon.com/dp/0262162091/

Followed by a 600 page book: http://www.amazon.com/dp/0262162288/

Professor Harper's own book (free! while in draft form), http://www.cs.cmu.edu/~rwh/plbook/book.pdf , is a better source for understanding the material in this post.

But, to be perfectly honest, I'm a systems-focused PL graduate student and have spent quite a bit of time studying this stuff and doubt that I could easily produce a more accessible version of this post. I tried (in the comments block here) and ran on to about two pages before realizing I had only covered the back story on his "trinity" analogy without even getting to this post itself. Someone far smarter than I probably could, but don't feel disappointed if you found this post mathematically challenging even if you normally follow PL theory. It took me a solid cup of coffee and a half an hour to deeply understand what he was saying.

Pierce's TAPL primarily covers the type side of this "trinity" and TAPL2 really only has one relevant chapter, covering Dependent Types.

Neither of which deal directly with Homotopy Type theory AFAIK.

This commenter on reddit did a good job: http://www.reddit.com/r/programming/comments/hnh59/ask_progg...

Reply on news.ycombinator.com