Lambda the Ultimate

USPS, not UPS, so it might take a bit longer than I had thought. Still, I said I'd review it, so unless someone else beats me to it... :-)

First impressions:

Scott's right: it isn't so much "Advanced Topics in Types and Programming Languages" as "Topics in Advanced Types and Programming Languages." This is emphatically a good thing from the perspective of this industry practitioner who's more interested in understanding what new languages might do than in proving that any given type system does or does not have certain properties, although, as always, it's nice to know that the proofs exist in the event I eventually care enough to check them.

Scott's also correct that Benjamin Pierce's deft hand as an editor is in evidence.

On to the content. The book is divided into five sections. Section I, "Precise Type Analyses," is composed of the first three chapters.

Chapter 1 deals with substructural type systems. The subject is well-motivated, making the point that such systems disallow operations on objects in an invalid state, e.g. reading a file that's closed, accessing freed memory, etc. The chapter begins with a brief review of the simply-typed lambda calculus; discusses the structural properties of exchange, weakening, and contraction; and then describes how substructural type systems consist of removing one or more of these properties, and what effect this has. Various extensions and variants are then described—in fact, they comprise most of the chapter. Finally, the chapter includes rather copious notes that, among other things, connect the chapter to others in the book, particularly those on dependent types and effects.

Chapter 2, on dependent types, makes my brain hurt, perhaps because I have not yet developed the necessary intuitions to be able to keep the various levels denoted in the rules separated in my head. Indeed, the chapter itself makes this point in motivating its investigation of Pure Type Systems. By the time I got to Figure 2-9, I certainly was ready for it! I'm a bit surprised that the author neglected to discuss Uniform Pure Type Systems and the Open Calculus of Constructions, which, from an implementation point of view, would seem to me to have some advantages over PTSs that abstract from names and the Calculus of Constructions or Calculus of Inductive Constructions. I like the idea of being able to treat everything as a set of rewrite rules, but I guess "up to α-conversion" is just seared into everyone's brain.

Chapter 3, covering effect types and region-based memory management, is perhaps the most pragmatic in the book, since nearly everyone agrees that memory safety is a desirable property, but not necessarily that garbage collection is the best way to achieve that goal in all cases. The treatment of effects within a type system may also come as a surprise to those who associate type theory primarily with more-or-less-pure functional programming, but effect systems have applications in, e.g. cryptographic protocol verification that would be difficult to accomplish in other ways. The chapter closes with extensive discussions of the ML Kit and Cyclone, two mature systems employing effect types and region-based memory management.

Part II, "Types for Low-Level Languages," consists of chapters 4 and 5.

Chapter 4 covers Typed Assembly Language. Much of the chapter is devoted to describing how memory safety can be accomplished in an assembly language with a relatively simple type system. Section 4.7 briefly describes extensions to support more practical language features such as objects and closures, and Section 4.7 treats "Some Real World Issues." Perhaps it's due to where my own interests lie, but this strikes me as the thinnest chapter in the book. In fairness, that may also be due to the subject matter being quite new relative to some of the other applications of type theory, and the chapter does serve effectively, in my opinion, as a prolegomenon to chapter 5.