|
http://www.spinellis.gr/pubs/Breview/2003-CR-TAPL/html/review.html 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:
|
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.
