What do you think?
Rate this book
Advanced Topics in Types and Programming Languages by Pierce, Benjamin C (2005) Hardcover
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.
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.
Hardcover
First published January 1, 2002
161 people are currently reading
3,014 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 24 of 24 reviews
July 10, 2014
One of my most unpleasant experience in grad school is when I has absolutely no idea what his peers are talking about. I frequently found myself in that situation during my years at CMU. Type theory is one of the topics. Why didn’t I just ask them? I did. My friend Oliver once gave me the perfect response: “I cannot afford to spend time on educating you.� In a world full of distractions and useless information, time is very valuable resource. If one wants to learn, he has to spend his own time
That is why I picked up the Benjamin Pierce’s book after many years of random embarrassments. I am glad that I did it. The book is really a fun read. And it really is nice written. Having read some technical books from both engineering and computer science categories, I have always found the computer science books more enjoyable and, in some sense, entertaining. For example, many hard core computer science books deliberately puts some effort in telling the history of the technology. And computer science people like to decorate the text with a few fun quotes. They all make the reading and learning more fun.
The book is very well written. By very well, I mean 1) it spend enough effort on the basics. It elaborates all the details and mathematical backgrounds that one need to acquire. 2) It develop the framework in a nicely slow, step-by-step pace. Every chapter is a very small enhancement over the last few chapters. And the author even takes the time to highlight the newly added rules in the type system. 3) It gives appropriate references for further reading. I did not check the references, but from the text it sure looks appropriate and thorough. 4) It has all the details of the proof, if one prefer, he/she can check the proofs themselves.
I like the book mainly because it makes me appreciate the type system. I remember the frustration that I had when I was writing some C++ template program. Not to mention the times that I was scratching my head over some weird OCaml type errors. A year ago I was fully convinced type checking is a complete pain in the butt; it slows us developers down and we should all write in Python, Ruby or MATLAB. But now I changed my mind. When Herb Sutter says ‘type system is your friend� on channel 9, I tend to agree with him.
That is why I picked up the Benjamin Pierce’s book after many years of random embarrassments. I am glad that I did it. The book is really a fun read. And it really is nice written. Having read some technical books from both engineering and computer science categories, I have always found the computer science books more enjoyable and, in some sense, entertaining. For example, many hard core computer science books deliberately puts some effort in telling the history of the technology. And computer science people like to decorate the text with a few fun quotes. They all make the reading and learning more fun.
The book is very well written. By very well, I mean 1) it spend enough effort on the basics. It elaborates all the details and mathematical backgrounds that one need to acquire. 2) It develop the framework in a nicely slow, step-by-step pace. Every chapter is a very small enhancement over the last few chapters. And the author even takes the time to highlight the newly added rules in the type system. 3) It gives appropriate references for further reading. I did not check the references, but from the text it sure looks appropriate and thorough. 4) It has all the details of the proof, if one prefer, he/she can check the proofs themselves.
I like the book mainly because it makes me appreciate the type system. I remember the frustration that I had when I was writing some C++ template program. Not to mention the times that I was scratching my head over some weird OCaml type errors. A year ago I was fully convinced type checking is a complete pain in the butt; it slows us developers down and we should all write in Python, Ruby or MATLAB. But now I changed my mind. When Herb Sutter says ‘type system is your friend� on channel 9, I tend to agree with him.
January 15, 2013
After spending years on my shelf and having been partially read at least once before, this book was finally finished! (I don't know why I used the passive form there, it just felt right for some reason)
I'm glad I did finally read it, even though there were parts that were glanced through without too much attention to detail and even though I skipped the exercises that are probably needed to get a more thorough understanding of the material. I read it mostly as a way to get a good overview of the basics of typed lambda calculi, which the book supplies with a focus on the use of such formalism in the specification and analysis of programming languages. The book is divided into six major parts which all deal with increasing levels of complexity in type systems. The first part introduces untyped formal calculi, first simple arithmetic expressions, then the classic lambda calculus. After this follows a part of simply typed lambda calculi which begins with nothing but function types and later expands this with base types and different structured types such as pairs, tuples, records, lists and other common forms of types. The next major part deals with subtyping and how it interacts with the forms of types presented so far, and after that there's a part of recursive types. While the expansions to the simply typed lambda calculus introduced so far have lots of interesting uses as well as theoretical properties, neither of them introduces something really new in the expressiveness of the language, at least nothing as important as the polymorphism introduced in part five. The reason I value this so much higher is that it enables a completely new form of abstraction. All the systems introduces before this have only the basic function abstraction on the level of terms, but with polymorphism, the ability to abstract over types in terms is introduced (the first step to move away from the first corner of the Barendregt, or lambda, cube which we will talk more about soon). Polymorphism through both universal and existential quantification is presented in different forms and at the end of the part, polymorphism is combined with subtyping in a non-trivial way yielding bounded quantification. Finally, the book is ended with a short part on higher-order systems featuring type operators and kinding (a way to classify the level of types in terms of kinds in the same way that term-level expressions are classified by types) constituting another move in the Barendregt cube where we can now abstract over types in type expressions. The final move possible in the cube, yielding dependent types (abstraction over term-level expressions in types) is also briefly mentioned but not worked out formally as the rest are.
The Barendregt cube is a unifying way to look at the expressiveness possible in the different type systems presented here and elsewhere, and another interesting and unifying theme is that of the Curry-Howard isomorphism, stating that there is a correspondence between programs and proofs on the one hand and types and propositions on the other so that a program having a certain type in a formal calculus corresponds to a proof of a corresponding proposition in a logic. This is discussed at many point throughout the book, giving historical explanations of how the correspondence between specific logics and corresponding type systems have been invented/discovered (depending on your particaular view on philosophy of mathematics and/or logic).
It's a fairly theoretical text, but with many examples, the type systems are not presented as pure formalisms but are motivated through code examples in the calculi presented and at three different points in the book, attempts at formalizing object-oriented concepts in the calculi are presented with increasing sophistication as the new expressive power of the formalisms developed allows it.
As an overview of the formal specifications of programming languages, their syntax and semantics (with a special focus on type systems), along with practical motivations, some points on implementations (almost all the formalisms introduced have actual accompanying implementations to be downloaded from the book's website), proofs of metatheoretic properties and comparisons with some actual programming languages, the book could hardly be better. The only reason that I'm not giving it five stars is that I reserve that for books that are almost perfect, and this does not quite live up to such a high standard. For example, the sometimes very technical proofs are a bit too dense for my taste. Towards the end of the book, there are some attempts at giving a more intuitive sense for some of the formalisations by presenting some of the mechanisms in an anthropomorphic way, by describing a function as saying something along the lines of "give me a value of such and such type, along with a function... and I will apply the function to produce a result..." which I appreciated highly. Had the whole book attempted to present things in such a manner more, had the author stopped now and then to discuss things in a more intuitive way, then I probably would have given it five stars. As it is though, it's an excellent book that I highly recommend for anyone interested in the subject.
I'm glad I did finally read it, even though there were parts that were glanced through without too much attention to detail and even though I skipped the exercises that are probably needed to get a more thorough understanding of the material. I read it mostly as a way to get a good overview of the basics of typed lambda calculi, which the book supplies with a focus on the use of such formalism in the specification and analysis of programming languages. The book is divided into six major parts which all deal with increasing levels of complexity in type systems. The first part introduces untyped formal calculi, first simple arithmetic expressions, then the classic lambda calculus. After this follows a part of simply typed lambda calculi which begins with nothing but function types and later expands this with base types and different structured types such as pairs, tuples, records, lists and other common forms of types. The next major part deals with subtyping and how it interacts with the forms of types presented so far, and after that there's a part of recursive types. While the expansions to the simply typed lambda calculus introduced so far have lots of interesting uses as well as theoretical properties, neither of them introduces something really new in the expressiveness of the language, at least nothing as important as the polymorphism introduced in part five. The reason I value this so much higher is that it enables a completely new form of abstraction. All the systems introduces before this have only the basic function abstraction on the level of terms, but with polymorphism, the ability to abstract over types in terms is introduced (the first step to move away from the first corner of the Barendregt, or lambda, cube which we will talk more about soon). Polymorphism through both universal and existential quantification is presented in different forms and at the end of the part, polymorphism is combined with subtyping in a non-trivial way yielding bounded quantification. Finally, the book is ended with a short part on higher-order systems featuring type operators and kinding (a way to classify the level of types in terms of kinds in the same way that term-level expressions are classified by types) constituting another move in the Barendregt cube where we can now abstract over types in type expressions. The final move possible in the cube, yielding dependent types (abstraction over term-level expressions in types) is also briefly mentioned but not worked out formally as the rest are.
The Barendregt cube is a unifying way to look at the expressiveness possible in the different type systems presented here and elsewhere, and another interesting and unifying theme is that of the Curry-Howard isomorphism, stating that there is a correspondence between programs and proofs on the one hand and types and propositions on the other so that a program having a certain type in a formal calculus corresponds to a proof of a corresponding proposition in a logic. This is discussed at many point throughout the book, giving historical explanations of how the correspondence between specific logics and corresponding type systems have been invented/discovered (depending on your particaular view on philosophy of mathematics and/or logic).
It's a fairly theoretical text, but with many examples, the type systems are not presented as pure formalisms but are motivated through code examples in the calculi presented and at three different points in the book, attempts at formalizing object-oriented concepts in the calculi are presented with increasing sophistication as the new expressive power of the formalisms developed allows it.
As an overview of the formal specifications of programming languages, their syntax and semantics (with a special focus on type systems), along with practical motivations, some points on implementations (almost all the formalisms introduced have actual accompanying implementations to be downloaded from the book's website), proofs of metatheoretic properties and comparisons with some actual programming languages, the book could hardly be better. The only reason that I'm not giving it five stars is that I reserve that for books that are almost perfect, and this does not quite live up to such a high standard. For example, the sometimes very technical proofs are a bit too dense for my taste. Towards the end of the book, there are some attempts at giving a more intuitive sense for some of the formalisations by presenting some of the mechanisms in an anthropomorphic way, by describing a function as saying something along the lines of "give me a value of such and such type, along with a function... and I will apply the function to produce a result..." which I appreciated highly. Had the whole book attempted to present things in such a manner more, had the author stopped now and then to discuss things in a more intuitive way, then I probably would have given it five stars. As it is though, it's an excellent book that I highly recommend for anyone interested in the subject.
September 20, 2012
I liked the structure: starting simple, explaining things clearly, and building slowly.
Don't attempt to read this book without at least a basic knowledge of doing proofs in math and higher-order logic. This should cover you:
As you work on implementing your own type systems, you'll find the detailed metatheory chapters worth revisiting.
Don't attempt to read this book without at least a basic knowledge of doing proofs in math and higher-order logic. This should cover you:
As you work on implementing your own type systems, you'll find the detailed metatheory chapters worth revisiting.
Want to read
May 17, 2007Perhaps the best book of its kind for the beginning/intermediate programmer interested in PLT (programming language theory). The book covers the simple untyped lambda calculus and builds on that foundation to many typed lambda calculi. Implementation chapters show the reader how to put the information to good use, providing executable code in the O'Caml language.
As a non-mathematician, programming hobbyist without formal experience or training, I've found this book particularly helpful in following along with discussion between academics. This is a book I pick up every once and a while to remind myself of the basics. Developing an intuition for the concepts described in the earlier chapters of the book is non-trivial, but essential to understanding concepts described later on.
As a non-mathematician, programming hobbyist without formal experience or training, I've found this book particularly helpful in following along with discussion between academics. This is a book I pick up every once and a while to remind myself of the basics. Developing an intuition for the concepts described in the earlier chapters of the book is non-trivial, but essential to understanding concepts described later on.
October 17, 2024
I mean, it's TAPL. There are probably better resources (now) if the goal is simply to implement something (e.g., algorithm W), but TAPL offers a comprehensive introduction to type theory with virtually zero prerequisites. I also just really enjoy Pierce's writing. One frustrating aspect is the amount of text dedicated to subtyping/Java; I guess that's just a consequence of the book being released in the dark ages when people thought OOP was relevant at all.
August 29, 2008
An absolute necessity for anyone wanting to learn the theoretical underpinnings of programming languages.
January 12, 2024
A surprisingly lucid and readable textbook. It slowly built up everything I needed to know and I'm kind of amazed how much I learned. The exercises were a nice mix of quick understanding checks and longer proofs/constructions. I read this to brush up before attending PoPL.
May 15, 2014
A canonical tome. If you're writing a type system, read this.
March 20, 2014
I doubt that I would have gotten total understanding even if I hade made the exercises, but still, I got a lot of understanding about type systems and the kind of things there are to consider.
June 13, 2016
It's awesome. Personally sub-typing and implementing Java wasn't interesting to me but everything else was.
June 17, 2024
Verbose, long winded, explaining of a very boring type of theoretical computer science. Often could've been shortened by just presenting a lovely proof instead of taking detours and bloating the essence of what it is. Better of starting with Number theory, Category Theory then flicking through the proofs on this one, before implementing a compiler. Would be a lot faster and more fun to learn that way, and refer back to "theoretically perfect types," here. In practice being "mathematically," correct while offering safety, makes it more restrictive, and popular languages don't follow it 100%. Something you can only understand why after implementation of some dummy languages. Would've been a 4 had it been more consise.
November 12, 2022
This is a review of the 2nd edition, it might not be applicable to the 3rd edition.
It's hard to evaluate this book. Often you will have to skip forward and backward to find the definition to some terms or theorems that were only mentioned in passing. Other times important concepts are just not described at all despite their importance. For example "coinduction" in chapter 21 is never rigorously defined or given examples to, despite having a very long chapter dedicated to it. In fact this chapter, despite its importance, rapidly hops through concepts based on lattice theories (such as the Knaster-Tarski theorem) without explaining how or why they are relevant to the topic at hand (a few examples here would have helped). Another example is the "X" subscript variables in chapter 22. There's just no definition of it and you're either supposed to figure this out yourself or read another material.
Otherwise, the book is comprehensive in the way you expect from an introductory book. There's barely any prerequisite to reading it. I honestly don't know if there's another book of the same sort so there's no comparison to be made. If you're interested in this topic, you'll probably end up reading this anyway, irregardless to its quality.
It's hard to evaluate this book. Often you will have to skip forward and backward to find the definition to some terms or theorems that were only mentioned in passing. Other times important concepts are just not described at all despite their importance. For example "coinduction" in chapter 21 is never rigorously defined or given examples to, despite having a very long chapter dedicated to it. In fact this chapter, despite its importance, rapidly hops through concepts based on lattice theories (such as the Knaster-Tarski theorem) without explaining how or why they are relevant to the topic at hand (a few examples here would have helped). Another example is the "X" subscript variables in chapter 22. There's just no definition of it and you're either supposed to figure this out yourself or read another material.
Otherwise, the book is comprehensive in the way you expect from an introductory book. There's barely any prerequisite to reading it. I honestly don't know if there's another book of the same sort so there's no comparison to be made. If you're interested in this topic, you'll probably end up reading this anyway, irregardless to its quality.
July 26, 2017
Didn’t really finish—super dense stuff, putting me to sleep after a page or so. Will have to re-read a few more times, if I ever need it.
This entire review has been hidden because of spoilers.
October 21, 2017
Very good introduction into theory of types. Useful if your dealing with modern software development tools, like Kotlin, Facebook's Flow, Haskell, Typescript.
Read
September 19, 2022just a skim to get oriented
January 18, 2024
An interesting introduction. I felt some topics were glanced over too quickly and that the definitions were lacking for such a precise topic. I feel like it's a decent starting point to the subject.
August 16, 2021
Great introduction to type systems and runtime semantics of PLs. Doesn't cover dependent type systems, type inference beyond Hindley-Milner, or practical problems of compilation to assembly languages.
August 27, 2008
An invaluable reference for programming language theory. Especially useful for those interested in functional languages, which seem to be poorly covered elsewhere. This book works in the opposite direction as most, assuming a functional approach and eventually deriving imperative constructs, rather than the other way around. I like this much better, but it may be tough if you lack the functional background.
One thing I've noticed is that people seem to get hung up over the notation and liberal use of Greek symbols. If you've taken a logic class (and don't have symbolphobia), you should be fine. If you haven't, it's not hard to figure out with some initial effort, and it's very consistent throughout.
One thing I've noticed is that people seem to get hung up over the notation and liberal use of Greek symbols. If you've taken a logic class (and don't have symbolphobia), you should be fine. If you haven't, it's not hard to figure out with some initial effort, and it's very consistent throughout.
Read
November 14, 2019Excellent. A small note: if (like me) you get bogged down in the proofs, Pierce's may be a better introduction to ideas such as type preservation, progress properties, and induction over terms and type derivations. I wish I'd read that work first.
August 10, 2013
Awesome book, particularly if you like programming languages.
Also, the proof exercises are good at training your brain for combinatorial reasoning. It helps to makes reasoning about programing languages intuitive.
I loved this book.
Also, the proof exercises are good at training your brain for combinatorial reasoning. It helps to makes reasoning about programing languages intuitive.
I loved this book.
February 3, 2017
Very clear & accessible intro to programming language theory. Lots of late-night fun to be had here.
Make sure you check out the OCaml code that accompanies it. It provides just enough motivation & examples to keep going through the theory in the actual text.
Make sure you check out the OCaml code that accompanies it. It provides just enough motivation & examples to keep going through the theory in the actual text.
Want to read
December 12, 2008Brian Goetz's favorite CS book -
March 5, 2009
A classic in Type Theory, it gives you background in something modern programmers are woefully and shamefully ignorant in.
January 19, 2014
very dense and theory heavy. but interesting, none the less.
Displaying 1 - 24 of 24 reviews
Can't find what you're looking for?
Get help and learn more about the design.