3 ms·
Higher-Dimensional Type Theory
- dolvlo 15y agoAnyone want to explain this using less jargon?
- davidmathers 15y agoWell, Benjamin Pierce has a 600 page book: http://www.amazon.com/dp/0262162091/ http://www.amazon.com/dp/0262162091/ Followed by a 600 page book: http://www.amazon.com/dp/0262162288/ http://www.amazon.com/dp/0262162288/
- larsberg 15y agoProfessor Harper's own book (free! while in draft form), http://www.cs.cmu.edu/~rwh/plbook/book.pdf 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.
- fogus 15y agoNeither of which deal directly with Homotopy Type theory AFAIK.
- jdminhbg 15y agoThis commenter on reddit did a good job: http://www.reddit.com/r/programming/comments/hnh59/ask_proggit_could_someone_explain_this_to_me_type/c1wso7w http://www.reddit.com/r/programming/comments/hnh59/ask_progg...
- ghotli 15y agoThis is the kind of thing I like to see on HN.
- coconutrandom 15y agoFor a second I was imagining Helvetica in 4D+
- primodemus 15y agoFor the interested, Steve Awodey has an introductory article, with pointers to the relevant literature: http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf
- moultano 15y agoEvery 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. :)
- cyrus_ 15y agoA 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.