Types and Programming Languages (Hardcover)

~ (Author)

Editorial Reviews

Review

"Types are the leaven of computer programming; they make it digestible. This excellent book uses types to navigate the rich variety of programming languages, bringing a new kind of unity to their usage, theory, and implementation. Its author writes with the authority of experience in all three of these aspects."
—Robin Milner, Computer Laboratory, University of Cambridge

Product Description

A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective—-has important applications in software engineering, language design, high-performance compilers, and security. This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material. The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.

See all Editorial Reviews

Product Details

• Hardcover: 645 pages
• Publisher: The MIT Press; 1 edition (February 1, 2002)
• Language: English
• ISBN-10: 0262162091
• ISBN-13: 978-0262162098
• Product Dimensions: 9.1 x 8.3 x 1.3 inches
• Shipping Weight: 2.9 pounds (View shipping rates and policies)
• Average Customer Review: 4.8 out of 5 stars  See all reviews (6 customer reviews)
• Amazon.com Sales Rank: #54,740 in Books (See Bestsellers in Books)

• This is item 1 in The Types and Programming Languages Series.

Customer Reviews

Most Helpful Customer Reviews

34 of 36 people found the following review helpful:

5.0 out of 5 stars An accessible yet thorough introduction to type systems, December 29, 2002

By	Jason M Kinzer (Oklahoma City, OK USA) - See all my reviews

This text is perhaps the most accessible yet thorough introduction to type systems I've encountered.

On the one hand, it offers excellent grounding: practical motivation is provided, numerous examples illustrate the concepts, and implementations are provided which can be used to typecheck and evaluate these examples. At various points, extended demonstrations of the type systems under consideration are given (e.g. showing how objects may be encoded). The exercises are well constructed and in many cases, accompanied with answers and detailed explanations in the appendix.

On the other hand, it offers an excellent exposition of the material: Pierce provides a lucid account of the static and dynamic semantics (primarily small-step operational) for various lambda calculi. He proceeds in a stepwise fashion via the gradual accretion of features: from first order (simply typed) systems to higher order systems incorporating bounded subtyping and recursion. He also gives attention to the metatheory of these systems (focusing on proofs of progress and preservation, and for systems with subtyping, of decideability). Internally, the text is well organized, with clear dependencies among the chapters, and the bibliography is extensive.

It should be noted that, while reasonably comprehensive, the text is necessarily limited in scope. For example, aside from the discussion on Featherweight Java, systems other than typed lambda calculus variants are not considered. In my opinion, the focus on these (in some sense "low-level") calculi makes foundational issues more apparent, and the linear progression from simple to complex variants lends a pleasant cohesiveness that would have been lost in a more general survey. However, as object/class encodings were discussed at various points, it would have been nice to see a more integrated presentation, in the spirit of the paper Comparing Object Encodings [BCP97].

7 of 7 people found the following review helpful:

5.0 out of 5 stars Just right, June 3, 2007

By	Jason Orendorff (Nashua, NH USA) - See all my reviews (REAL NAME)

This is a textbook about programming language theory, somewhat mathematical-- but it's must-read material for anyone who wants to gripe about programming languages cluefully, much less design them.

For me, this book strikes exactly the right balance between theory and practicality. Chapters on the mathematical properties of various tiny programming languages are interleaved with chapters that provide annotated implementations of those languages.

The book will also give you the background (notation and terminology) you'll need to read cutting-edge research papers on programming language theory.

This book contains all the information I was missing. Excellent presentation of the material, well written, great exercises, doesn't go off into lala-land. Highly recommended. Some math background very helpful (you need to know what a mathematical proof is).

11 of 13 people found the following review helpful:

5.0 out of 5 stars Well put, practical and theoretic book on types., December 21, 2004

By	S. van den Berg "Functional programmer" (Schagen, NH Netherlands) - See all my reviews

Extremely well written book on type systems in programming languages. Uses lambda calculus to explain type systems. Practical aspects show up in the ML implementations downloadable on the books site.
Contains a lot of programming language theory besides just type-systems. Can be used as an introductionary book to programming language design. Concluding: Great book!