Types and Programming Languages

Citation

Pierce, B. C. (2002). Types and Programming Languages. The MIT Press.

Chapter Summary

The book has thirty-two chapters in six parts, preceded by an introduction (Chapter 1) and a short chapter of mathematical preliminaries (Chapter 2), and followed by two appendices: solutions to selected exercises (about 70 pages) and notational conventions. Several chapters are implementation chapters, each titled "An ML Implementation of ..." and each paired with the theory chapter before it.

Chapters 1–2: Introduction; Mathematical Preliminaries

Chapter 1 asks what types are in computer science and what type systems are good for, how they relate to language design, and gives a capsule history and related reading. Chapter 2 reviews sets, relations and functions, ordered sets, sequences and induction.

Part I: Untyped Systems (Chapters 3–7)

Chapter 3, Untyped Arithmetic Expressions, introduces syntax, induction on terms, semantic styles and evaluation using a tiny language. Chapter 4 is its ML implementation. Chapter 5, The Untyped Lambda-Calculus, covers the basics, programming in the lambda-calculus and the formal definitions; Chapter 6 gives a nameless representation of terms using shifting and substitution; Chapter 7 implements the lambda-calculus in ML.

Part II: Simple Types (Chapters 8–14)

Chapter 8, Typed Arithmetic Expressions, introduces types and the typing relation and states safety as progress plus preservation. Chapter 9, Simply Typed Lambda-Calculus, adds function types, properties of typing, the Curry–Howard correspondence, erasure and typability, and Curry-style versus Church-style presentations; Chapter 10 implements the type checker. Chapter 11, Simple Extensions, adds base types, unit, sequencing, ascription, let bindings, pairs, tuples, records, sums, variants, general recursion and lists. Chapter 12, Normalization, proves normalization for simple types. Chapter 13, References, and Chapter 14, Exceptions, extend the language with mutable state (with store typings and a safety proof) and with raising and handling exceptions.

Part III: Subtyping (Chapters 15–19)

Chapter 15, Subtyping, covers subsumption, the subtype relation, its interaction with typing, top and bottom types, other features, coercion semantics, and intersection and union types. Chapter 16 gives the metatheory (algorithmic subtyping and typing, joins and meets); Chapter 17 the ML implementation. Chapters 18 and 19 are case studies: Imperative Objects, which builds object-oriented features such as classes, self and open recursion from the calculus, and Featherweight Java, a core calculus that also serves to discuss nominal versus structural type systems.

Part IV: Recursive Types (Chapters 20–21)

Chapter 20 introduces recursive types with examples, formalities and subtyping. Chapter 21, Metatheory of Recursive Types, develops induction and coinduction, finite and infinite types, membership checking, regular trees, μ-types and subtyping of iso-recursive types.

Part V: Polymorphism (Chapters 22–28)

Chapter 22, Type Reconstruction, covers type variables and substitutions, constraint-based typing, unification, principal types and let-polymorphism. Chapter 23, Universal Types, introduces System F, its examples and properties, erasure, fragments, parametricity and impredicativity. Chapter 24, Existential Types, treats data abstraction with existentials and their encoding; Chapter 25 implements System F. Chapter 26, Bounded Quantification, defines it with examples and a safety proof; Chapter 27 revisits imperative objects with the new tools; Chapter 28 treats its metatheory, including the undecidability of full F<:.

Part VI: Higher-Order Systems (Chapters 29–32)

Chapter 29, Type Operators and Kinding, introduces kinds; Chapter 30, Higher-Order Polymorphism, studies the resulting system and ends with a section on dependent types; Chapter 31 covers higher-order subtyping. Chapter 32, Case Study: Purely Functional Objects, builds an object encoding from these ingredients.

Key Concepts

Parts I and II

• Operational semantics and induction on terms: defining evaluation by rules and proving properties by induction over syntax.
• Safety as progress plus preservation: the standard way of showing that well-typed programs do not get stuck.
• Curry–Howard correspondence: the link between types and propositions, and between programs and proofs.
• Normalization: every well-typed term of the simply typed calculus evaluates to a value.

Parts III and IV

• Subsumption and the subtype relation: using a term of a subtype wherever a supertype is expected.
• Algorithmic subtyping: turning declarative rules into a decidable procedure.
• Induction and coinduction: the proof principles needed for recursive types.

Parts V and VI

• Type reconstruction and let-polymorphism: inferring types by constraints and unification.
• System F and parametricity: universal quantification over types.
• Bounded quantification (F<:): combining polymorphism with subtyping.
• Kinds and type operators: classifying types themselves, the basis of higher-order systems.

Critical Analysis

Strengths

• Pragmatic, motivated approach. The author's own description is that each new concept is motivated by programming examples and that the more theoretical sections are driven by the needs of implementations. The case studies on objects show features of real languages explained through the formal systems.
• Implementations alongside the theory. Chapters 4, 7, 10, 17 and 25 are implementation chapters, and the author's site offers working type checkers for most of the calculi, written in OCaml, for experimenting and for testing exercise solutions.
• Explicit dependencies. The description says dependencies between chapters are stated explicitly, so readers can choose different paths through the material.
• Exercises with solutions. Each chapter has exercises, and Appendix A gives solutions to selected ones over about 70 pages. Endorsements on the author's page from Robin Milner, Robert Harper, John Reynolds and Henk Barendregt describe the book as clear, well organized and spanning both theory and implementation, with exercises from easy to challenging.

Limitations

• Mathematical demands. The book is built from definitions, induction proofs and metatheory; readers need comfort with that style, as Chapter 2 only reviews the preliminaries.
• Scope ends at the early 2000s. Dependent types receive one section (30.5), and the table of contents has no chapters on, for example, gradual typing or substructural systems.
• Uneven pace. Later chapters, such as 21 (recursive types metatheory, twelve sections) and 28 (bounded quantification), are far more technical than the early ones; the dependency structure is what makes it practical to skip them.

Where It Fits in the Course

Most books in this course are about building language processors. Nystrom's Crafting Interpreters walks through two complete interpreters for a small dynamically typed language. The Dragon Book, Cooper and Torczon's Engineering a Compiler, and Thain's compact undergraduate compiler text cover the stages from parsing to code generation. None of these is mainly about type theory; Pierce's book is the one that explains what a type system is and proves what it guarantees.

Read it after a course in which you have written an interpreter or compiler, or alongside one in logic or semantics. It assumes a reader who wants the formal view of languages that the others implement.

How to Use This Book

The book suits graduate students and advanced undergraduates in programming languages, researchers needing a precise account of standard type systems, and implementers who want type checking explained beyond one compiler. It rewards active reading: work the exercises.

A practical plan:

• Core: Chapters 1–3, 5, 8–9, 11 and 13–14 for the untyped and simply typed foundations.
• Next: Chapters 15–16 on subtyping and Chapters 22–23 on type reconstruction and System F.
• Optional paths: Chapters 18–19 (objects), 20–21 (recursive types), 24 (existentials), 26–28 (bounded quantification) and 29–32 (higher-order systems), chosen by interest using the chapter dependencies.

Run the OCaml implementations as each system is introduced and extend them, and use the solutions in Appendix A to check proofs. The errata list on the author's site is kept up to date.