This is an HTML rendering of a working paper draft that led to a publication. The publication should always be cited in preference to this draft using the following reference:

The document's metadata is available in BibTeX format.

Find the publication on Google Scholar

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Diomidis Spinellis Publications

Copyright © 2003 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or

Book review: Types and Programming Languages

Diomidis Spinellis
Athens University of Economics and Business

Benjamin C. Pierce
Types and Programming Languages
MIT Press, Cambridge, MA, USA, 2002
622 pp., ISBN 0262162091

Pierce defines as a type system "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.

The Types and Programming Languages book guides us through the rich and interesting field of type system design, reasoning, and implementation. Using operational semantics, and examples written in OCaml (Objective Caml)-available on-line 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 ML, relationships with mainstream languages such as Java and C++ are discussed as the related theory develops. Missing from the book is 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; Types and Programming Languages succeeds in bringing under one roof the most significant elements of a difficult but important computer science field.