3 ms·
I've been making my way through this book for the past few weeks; just started Chapter 20. I tried reading Harper's Practical Foundations for Programming Langu
by joel_dice 5y ago
I've been making my way through this book for the past few weeks; just started Chapter 20. I tried reading Harper's Practical Foundations for Programming Languages first, but it was too abstract for me, so I switched to TaPL.
What I like most about Pierce's book is that he introduces each concept with a formal, abstract definition, complete with proofs of correctness, but also follows that up with a concrete implementation in OCaml. The latter is very easy to follow if you've had some experience with the ML family of languages. I sometimes find myself skipping ahead to the OCaml version when I get lost in the math syntax, which for me is less familiar. I'm planning to come back to Harper's book later, but Pierce's book is the perfect fit for where I am now.
My only criticism is that some parts are very dated given it hasn't been updated in almost 20 years. In particular, the version of Java he discusses throughout the book (pre-generics, pre-type-inference) bears little resemblance to the modern one. And since 2002 we've seen affine types (e.g. Rust) start to have mainstream influence, among other things.
In case it's helpful, I'm compiling a list of resources as I learn type systems, logic, category theory, etc.:
https://gist.github.com/dicej/d1117e5d65155d750c16234e6eff1687 https://gist.github.com/dicej/d1117e5d65155d750c16234e6eff16...
- shadowfox 5y agoThere are somewhat more involved formal treatments like Welterweight Java [1], which adds some more features, but of course, nowhere near the full set of Java features. Some of the citations in that paper are also interesting. I don't think there is a core calculus that specifically incorporates generics as in Java, but I could be wrong. In any case, much of Java's generics flow from theories of parametric polymorphism [2], specifically I believe bounded parametric polymorphism [3]. [1] https://www.researchgate.net/publication/220877645_Welterweight_Java https://www.researchgate.net/publication/220877645_Welterwei... [2] https://www.cs.cmu.edu/~fp/courses/15814-f18/lectures/11-polymorphism.pdf https://www.cs.cmu.edu/~fp/courses/15814-f18/lectures/11-pol... [3] https://en.wikipedia.org/wiki/Bounded_quantification https://en.wikipedia.org/wiki/Bounded_quantification
- phlummox 5y agore: "I don't think there is a core calculus that specifically incorporates generics as in Java": doesn't Featherweight Java [1] already include generics? (Though a simplified version.) [1] https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf