|
|
|
|
|
|
by joel_dice
1684 days 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/d1117e5d65155d750c16234e6eff16... |
|
|
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_Welterwei...
[2] https://www.cs.cmu.edu/~fp/courses/15814-f18/lectures/11-pol...
[3] https://en.wikipedia.org/wiki/Bounded_quantification