A popular program on BBC Radio here in the UK is Desert Island Discs, where well-known personalities talk about their lives while choosing eight music tracks they consider significant. They also are asked to decide which book they would take with them to this island as their only reading material for the years to come.
This 800-page volume on lambda calculus could well be the desert island book of choice for anyone interested in the foundations of computation and mathematical logic. It can easily provide days, months, and maybe even years of entertainment, education, and mental challenge. This is due not only to the size of the book, but also to its mathematical density: on many pages, more of the content is formatted in LaTeX math mode than as paragraphs. Some very dense books can be difficult to follow, but I found the material here to be at the right level of granularity, allowing anyone with a modicum of graduate-level mathematical sophistication to follow the developments, with some time and effort. After all, the languages being described are simple and elegant.
The authors talk about their intention to inspire readers and to “reveal unexpected mathematical beauty.” I think they have succeeded in this goal, without decreasing the rigor of their treatment of the languages or of the proofs of interesting properties. Producing this book must have been a huge task. It weaves together research by prominent experts over the last few decades while keeping a consistent flow and style. The three main authors acknowledge the contribution of a handful of other authors, but take credit for the rigorous editing.
The book is divided into three parts, which address three distinct contributions to typing systems for lambda calculus: simple types, recursive types, and intersection types. Because of the history of each concept, each part has a distinct flavor. Part 1 covers simple types, which are well established, and shows the range of elaborations that can be made by logicians (proofs of consistency, normalization, decidability, and so on). Applications in programming and proof theory are also introduced. The techniques used are well established and well worth understanding. Part 2 is concerned with recursive types, which are well suited to be studied through type algebras. This represents a subtle shift of emphasis from lambda calculus terms to the type expressions themselves. The chapter on subtyping and programming languages is quite topical, as language designers are still struggling to give their type disciplines a solid foundation. Part 3 is about intersection types, for which a variety of type systems have been developed independently. Rather than concentrate on any one of these, the authors collectively explore mathematical models that could be used to examine the commonalities and distinctions between the systems.
When there are several ways of expressing some concept, the authors acknowledge this clearly and try to develop the different approaches. Early on, they talk about the choice of implicit or explicit typing (that is, a la Curry or a la Church); later on, they discuss representing recursive types as simultaneous recursions or &mgr;-types. This broad view makes the book more useful.
Overall, this is a very satisfying book. I would have liked to see some kind of coherent summary at the end of the book, which seems to end quite abruptly at a very technical point. The volume is very well presented, particularly considering the minutiae of mathematical notation involved, but I was puzzled by the change in font size used for Sections 7.4.1 and 7.6, which was not done elsewhere. The book is well referenced, although there are two places I saw where the referencing is incomplete: Exercise 7.10, which just says “(Klop),” and Theorem 5.3.34, which refers to “(Gentzen (reference)).” But these are quibbles; a volume of this complexity is bound to have some small mistakes.
I recommend this book as a very useful reference to anyone who would like a consolidated description of many of the very interesting and beautiful aspects of type systems associated with lambda calculus. Researchers and graduate students will get a lot out of some dedicated engagement with the rigorous coverage of the topic.