Hacker News Reader

Comment by mananaysiempre | Hacker News Reader

> I found that there are not enough good teaching materials on type checkers -- e.g. the second edition of the Dragon Book lacks a type checker, which is a glaring hole IMO

Pierce’s Types and Programming Languages[1] is excellent. It starts with very little (if you understand basic set-theory notation, you’re probably OK), gets you to a pretty reasonable point, and just generally makes for very pleasant reading. You should probably pick something else if you want a hands-on introduction with an immediate payoff, but then you probably wouldn’t pick the Dragon Book, either.

[1] https://www.cis.upenn.edu/~bcpierce/tapl/

View on HN

TaPL really falls down when trying to bootstrap your way to understanding the notation. A lot of the notation and theory revolves around, essentially, implementing a concurrent virtual machine. I like the original algorithm W paper because it doesn't gloss this conceptual step: it is very much a virtual machine & you can see the authors handling the edge cases. The operational semantics in TaPL are (frankly) obtuse. Also, TaPL makes it seem like new features can be desugared to old features — and they can — but a little more prose explaining the feature's behavior directly without just tossing you into the semantic deep end would've made a much nicer text.

Everyone always says that, but I don't think it's a good intro :-) (e.g. I think the top comment in the lobste.rs thread is suffering from the type inference / functional bias, which is not necessarily due to TAPL, but it's a common thing I've noticed)

Right now I think Siek's book is better for what I want to do, though admittedly I didn't get that far into it, because my type checking project is way on the back burner

I would like to see any type checkers that people wrote after reading TAPL!

I’m writing one now as part of a hobby language project, about which I’ll do a Show HN once I have enough to share. I enjoyed Pierce but to your point I am going mostly down the functional route. Programming it in Python, with the book closed but after two readings I have what I need in my head (it clicked much better second time through).

Edit: This project (best fun I’ve had programming in a long while) is what got me sharing Eli Bendersky’s Unification post a couple of weeks back https://news.ycombinator.com/item?id=44938156

Reply on news.ycombinator.com