Advanced Topics in Types and Programming Languages

The long awaited sequel to Types and Programming Languages by Benjamin Pierce is out! Check it out here:
Advanced Topics in Types and Programming Languages.

It is available from amazon. I'm certainly getting a copy. TAPL was great!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Ordered. Thanks!

Chapter 7 Online


When someone gets their hands on this book, could they please post a review?



Mine's already shipped from Oregon to California by UPS ground, so I should have it relatively soon. I'll be happy to review it for the group.


I can hardly wait. Thanks!


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... :-)

Got my copy!

Picked it up at Powells' the other night. Have only read through the first couple of chapters, so far... initial comments.

* On a negative note, the binding of the book appears to be of low quality. I mentioned to the cashier, she replied "textbooks"... perhaps the textbook industry has found another way (besided constant revision and short print runs) to handicap the used book market.

* On a positive note, the book so far is very cohesive in its style, unusually so for what is essentially a collection of papers by different authors. Notation is consistent, and there aren't the abrupt changes of style between chapters that I have come to expect with books of such nature.

* The material so far is interesting. The word "advanced" in the title might be a bit misleading, as the material isn't really any more difficult than TAPL. Instead, it focuses on specific topics and extensions of type theory.

* Overall, I have enjoyed the book quite a bit.

I have more reading to do (both in this book and in TAPL), but so far the book is well worth the wait.


Arrived Yesterday...

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.