Hacker News Comments on
Types and Programming Languages (The MIT Press)
·
4
HN comments
- This course is unranked · view top recommended courses
Hacker News Stories and Comments
All the comments and stories posted to Hacker News that reference this book.Strongly recommend Types and Programming Languages [1]. I think it's the most useful + accessible book on type theory out there.[1] https://www.amazon.com/Types-Programming-Languages-MIT-Press...
Hmm, H-M, AKA Damas-Milner, p 331 in TAPL (indexed as D-M only, so easy to overlook, and I can't see where it's in Harper's Practical Foundations, AFAICT.As an aside, the other day i started flipping thru Harper's Lazy Eval writeup, and found it surprisingly readable, even if i was skipping reading the rules.
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
http://www.amazon.com/Types-Programming-Languages-Benjamin-P...
here is a book that will school you: http://www.amazon.com/Types-Programming-Languages-Benjamin-P...It is a great book, but a little dense. Its example language is a typed lambda calculus. This is both good and bad. The good: you can evaluate most expressions in your head or with a pencil. The bad: sometimes it is difficult to read without evaluating the expressions.
It is heavy on proofs and mathematics, but it does what it says: it introduces you to the basics of type theory as applied to programming languages.
Edit: an amazon reviewer pointed at http://www.amazon.com/Foundations-Object-Oriented-Languages-... as an alternative book. I haven't read it but it does look useful.
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/
⬐ fogusNeither of which deal directly with Homotopy Type theory AFAIK.⬐ larsbergProfessor 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.