Pierce defines a type system as “a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the types of values they compute.” Don’t let this formal definition lead you into believing that the significance of type systems is only theoretical. A type system is one of the most important aspects of a programming language’s design. It provides the foundation for the compiler, and sometimes the runtime system, to detect many programmer errors, thus avoiding unspecified behavior such as program crashes. Many of the security breaches we commonly see on the Internet are nothing more than type violations that are not properly detected. Programmers who switch to a strongly typed language often express their surprise when their programs “just work” without additional debugging.

This book guides us through the rich and interesting field of type system design, reasoning, and implementation. Using operational semantics, and examples written in Objective Caml (OCaml), available on the book’s associated Web site, Pierce navigates through an eclectic and wide selection of theoretical topics with clarity and consistency. Modern typography is wisely employed throughout the book to clearly express complicated lambda reduction sequences, operational semantics, and programming examples. Numerous exercises, of varying degrees of difficulty, and detailed references make the book useful to the mature undergraduate or graduate student and the researcher alike.

Pierce presents language features following a common pattern, going through motivating examples, formal definitions, proofs of basic properties, presentation of type checking algorithms and proofs of their soundness, completeness, and termination, and algorithm implementation. The topics covered include the formal representation of untyped arithmetic expressions using lambda calculus, simple types, subtyping, recursive types, polymorphism, and higher-order types. Although emphasis is placed on the type systems of functional languages such as Haskell and meta language (ML), relationships with mainstream languages such as Java and C++ are discussed as the related theory develops. Missing from the book is a survey chapter presenting the particular characteristics, advantages, and shortcomings of the type systems of widespread modern languages. Such a chapter would have placed the theory in a more practical setting, helping both students of programming languages and budding language designers. One must not be ungrateful however; the book succeeds in bringing together, between one set of covers, the most significant elements of a difficult but important computer science field.