Types and Programming Languages

by Pierce, Benjamin C.

• ISBN13: 9780262162098
• ISBN10: 0262162091
• Format: Hardcover
• Copyright: 2002-01-04
• Publisher: The MIT Press

Summary

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.

Author Biography

Benjamin C. Pierce is Professor of Computer and Information Science at the University of Pennsylvania.

Table of Contents

Preface	xiii
Introduction	1	(14)
Types in Computer Science	1	(3)
What Type Systems Are Good For	4	(5)
Type Systems and Language Design	9	(1)
Capsule History	10	(2)
Related Reading	12	(3)
Mathematical Preliminaries	15	(6)
Sets, Relations, and Functions	15	(1)
Ordered Sets	16	(2)
Sequences	18	(1)
Induction	19	(1)
Background Reading	20	(1)
I Untyped Systems	21	(68)
Untyped Arithmetic Expressions	23	(22)
Introduction	23	(3)
Syntax	26	(3)
Induction on Terms	29	(3)
Semantic Styles	32	(2)
Evaluation	34	(9)
Notes	43	(2)
An ML Implementation of Arithmetic Expressions	45	(6)
Syntax	46	(1)
Evaluation	47	(2)
The Rest of the Story	49	(2)
The Untyped Lambda-Calculus	51	(24)
Basics	52	(6)
Programming in the Lambda-Calculus	58	(10)
Formalities	68	(5)
Notes	73	(2)
Nameless Representation of Terms	75	(8)
Terms and Contexts	76	(2)
Shifting and Substitution	78	(2)
Evaluation	80	(3)
An ML Implementation of the Lambda-Calculus	83	(6)
Terms and Contexts	83	(2)
Shifting and Substitution	85	(2)
Evaluation	87	(1)
Notes	88	(1)
II Simple Types	89	(90)
Types Arithmetic Expressions	91	(8)
Types	91	(1)
The Typing Relation	92	(3)
Safety = Progress + Preservation	95	(4)
Simply Typed Lambda-Calculus	99	(14)
Function Types	99	(1)
The Typing Relation	100	(4)
Properties of Typing	104	(4)
The Curry-Howard Correspondence	108	(1)
Erasure and Typability	109	(2)
Curry-Style vs. Church-Style	111	(1)
Notes	111	(2)
An ML Implementation of Simple Types	113	(4)
Contexts	113	(2)
Terms and Types	115	(1)
Typechecking	115	(2)
Simple Extensions	117	(32)
Base Types	117	(1)
The Unit Type	118	(1)
Derived Forms: Sequencing and Wildcards	119	(2)
Ascription	121	(3)
Let Bindings	124	(2)
Pairs	126	(2)
Tuples	128	(1)
Records	129	(3)
Sums	132	(4)
Variants	136	(6)
General Recursion	142	(4)
Lists	146	(3)
Normalization	149	(4)
Normalization for Simple Types	149	(3)
Notes	152	(1)
References	153	(18)
Introduction	153	(6)
Typing	159	(1)
Evaluation	159	(3)
Store Typings	162	(3)
Safety	165	(5)
Notes	170	(1)
Exceptions	171	(8)
Raising Exceptions	172	(1)
Handling Exceptions	173	(2)
Exceptions Carrying Values	175	(4)
III Subtyping	179	(86)
Subtyping	181	(28)
Subsumption	181	(1)
The Subtype Relation	182	(6)
Properties of Subtyping and Typing	188	(3)
The Top and Bottom Types	191	(2)
Subtyping and Other Features	193	(7)
Coercion Semantics for Subtyping	200	(6)
Intersection and Union Types	206	(1)
Notes	207	(2)
Metatheory of Subtyping	209	(12)
Algorithmic Subtyping	210	(3)
Algorithmic Typing	213	(5)
Joins and Meets	218	(2)
Algorithmic Typing and the Bottom Type	220	(1)
An ML Implementation of Subtyping	221	(4)
Syntax	221	(1)
Subtyping	221	(1)
Typing	222	(3)
Case Study: Imperative Objects	225	(22)
What Is Object-Oriented Programming?	225	(3)
Objects	228	(1)
Object Generators	229	(1)
Subtyping	229	(1)
Grouping Instance Variables	230	(1)
Simple Classes	231	(2)
Adding Instance Variables	233	(1)
Calling Superclass Methods	234	(1)
Classes with Self	234	(1)
Open Recursion through Self	235	(2)
Open Recursion and Evaluation Order	237	(4)
A More Efficient Implementation	241	(3)
Recap	244	(1)
Notes	245	(2)
Case Study: Featherweight Java	247	(18)
Introduction	247	(2)
Overview	249	(2)
Nominal and Structural Type Systems	251	(3)
Definitions	254	(7)
Properties	261	(1)
Encodings vs. Primitive Objects	262	(1)
Notes	263	(2)
IV Recursive Types	265	(50)
Recursive Types	267	(14)
Examples	268	(7)
Formalities	275	(4)
Subtyping	279	(1)
Notes	279	(2)
Metatheory of Recursive Types	281	(34)
Induction and Coinduction	282	(2)
Finite and Infinite Types	284	(2)
Subtyping	286	(2)
A Digression on Transitivity	288	(2)
Membership Checking	290	(5)
More Efficient Algorithms	295	(3)
Regular Trees	298	(1)
μ-Types	299	(5)
Counting Subexpressions	304	(5)
Digression: An Exponential Algorithm	309	(2)
Subtyping Iso-Recursive Types	311	(1)
Notes	312	(3)
V Polymorphism	315	(122)
Type Reconstruction	317	(22)
Type Variables and Substitutions	317	(2)
Two Views of Type Variables	319	(2)
Constraint-Based Typing	321	(5)
Unification	326	(3)
Principal Types	329	(1)
Implicit Type Annotations	330	(1)
Let-Polymorphism	331	(5)
Notes	336	(3)
Universal Types	339	(24)
Motivation	339	(1)
Varieties of Polymorphism	340	(1)
System F	341	(3)
Examples	344	(9)
Basic Properties	353	(1)
Erasure, Typability, and Type Reconstruction	354	(3)
Erasure and Evaluation Order	357	(1)
Fragments of System F	358	(1)
Parametricity	359	(1)
Impredicativity	360	(1)
Notes	361	(2)
Existential Types	363	(18)
Motivation	363	(5)
Data Abstraction with Existentials	368	(9)
Encoding Existentials	377	(2)
Notes	379	(2)
An ML Implementation of System F	381	(8)
Nameless Representation of Types	381	(1)
Type Shifting and Substitution	382	(1)
Terms	383	(2)
Evaluation	385	(1)
Typing	386	(3)
Bounded Quantification	389	(22)
Motivation	389	(2)
Definitions	391	(5)
Examples	396	(4)
Safety	400	(6)
Bounded Existential Types	406	(2)
Notes	408	(3)
Case Study: Imperative Objects, Redux	411	(6)
Metatheory of Bounded Quantification	417	(20)
Exposure	417	(1)
Minimal Typing	418	(3)
Subtyping in Kernel F<:	421	(3)
Subtyping in Full F<:	424	(3)
Undecidability of Full F<:	427	(5)
Joins and Meets	432	(3)
Bounded Existentials	435	(1)
Bounded Quantification and the Bottom Type	436	(1)
VI Higher-Order Systems	437	(54)
Type Operators and Kinding	439	(10)
Intuitions	440	(5)
Definitions	445	(4)
Higher-Order Polymorphism	449	(18)
Definitions	449	(1)
Example	450	(3)
Properties	453	(8)
Fragments of Fw	461	(1)
Going Further: Dependent Types	462	(5)
Higher-Order Subtyping	467	(8)
Intuitions	467	(2)
Definitions	469	(3)
Properties	472	(1)
Notes	472	(3)
Case Study: Purely Functional Objects	475	(16)
Simple Objects	475	(1)
Subtyping	476	(1)
Bounded Quantification	477	(2)
Interface Types	479	(1)
Sending Messages to Objects	480	(1)
Simple Classes	481	(1)
Polymorphic Update	482	(3)
Adding Instance Variables	485	(1)
Classes with ``Self''	486	(2)
Notes	488	(3)
Appendices	491	(76)
A Solutions to Selected Exercises	493	(72)
B Notational Conventions	565	(2)
B.1 Metavariable Names	565	(1)
B.2 Rule Naming Conventions	565	(1)
B.3 Naming and Subscripting Conventions	566	(1)
References	567	(38)
Index	605