Types and Programming Languages Book

After spending years on my shelf and having been partially read at least once before, this book was finally finished! (I don't know why I used the passive form there, it just felt right for some reason)

I'm glad I did finally read it, even though there were parts that were glanced through without too much attention to detail and even though I skipped the exercises that are probably needed to get a more thorough understanding of the material. I read it mostly as a way to get a good overview of the basics of typed lambda calculi, which the book supplies with a focus on the use of such formalism in the specification and analysis of programming languages. The book is divided into six major parts which all deal with increasing levels of complexity in type systems. The first part introduces untyped formal calculi, first simple arithmetic expressions, then the classic lambda calculus. After this follows a part of simply typed lambda calculi which begins with nothing but function types and later expands this with base types and different structured types such as pairs, tuples, records, lists and other common forms of types. The next major part deals with subtyping and how it interacts with the forms of types presented so far, and after that there's a part of recursive types. While the expansions to the simply typed lambda calculus introduced so far have lots of interesting uses as well as theoretical properties, neither of them introduces something really new in the expressiveness of the language, at least nothing as important as the polymorphism introduced in part five. The reason I value this so much higher is that it enables a completely new form of abstraction. All the systems introduces before this have only the basic function abstraction on the level of terms, but with polymorphism, the ability to abstract over types in terms is introduced (the first step to move away from the first corner of the Barendregt, or lambda, cube which we will talk more about soon). Polymorphism through both universal and existential quantification is presented in different forms and at the end of the part, polymorphism is combined with subtyping in a non-trivial way yielding bounded quantification. Finally, the book is ended with a short part on higher-order systems featuring type operators and kinding (a way to classify the level of types in terms of kinds in the same way that term-level expressions are classified by types) constituting another move in the Barendregt cube where we can now abstract over types in type expressions. The final move possible in the cube, yielding dependent types (abstraction over term-level expressions in types) is also briefly mentioned but not worked out formally as the rest are.

The Barendregt cube is a unifying way to look at the expressiveness possible in the different type systems presented here and elsewhere, and another interesting and unifying theme is that of the Curry-Howard isomorphism, stating that there is a correspondence between programs and proofs on the one hand and types and propositions on the other so that a program having a certain type in a formal calculus corresponds to a proof of a corresponding proposition in a logic. This is discussed at many point throughout the book, giving historical explanations of how the correspondence between specific logics and corresponding type systems have been invented/discovered (depending on your particaular view on philosophy of mathematics and/or logic).

It's a fairly theoretical text, but with many examples, the type systems are not presented as pure formalisms but are motivated through code examples in the calculi presented and at three different points in the book, attempts at formalizing object-oriented concepts in the calculi are presented with increasing sophistication as the new expressive power of the formalisms developed allows it.

As an overview of the formal specifications of programming languages, their syntax and semantics (with a special focus on type systems), along with practical motivations, some points on implementations (almost all the formalisms introduced have actual accompanying implementations to be downloaded from the book's website), proofs of metatheoretic properties and comparisons with some actual programming languages, the book could hardly be better. The only reason that I'm not giving it five stars is that I reserve that for books that are almost perfect, and this does not quite live up to such a high standard. For example, the sometimes very technical proofs are a bit too dense for my taste. Towards the end of the book, there are some attempts at giving a more intuitive sense for some of the formalisations by presenting some of the mechanisms in an anthropomorphic way, by describing a function as saying something along the lines of "give me a value of such and such type, along with a function... and I will apply the function to produce a result..." which I appreciated highly. Had the whole book attempted to present things in such a manner more, had the author stopped now and then to discuss things in a more intuitive way, then I probably would have given it five stars. As it is though, it's an excellent book that I highly recommend for anyone interested in the subject.