1 Introduction 1
1.1 Types in Computer Science 1
1.2 What Type Systems Are Good For 4
1.3 Type Systems and Language Design 9
1.4 Capsule History 10
1.5 Related Reading 12
2 Mathematical Preliminaries 15
2.1 Sets， Relations， and Functions 15
2.2 Ordered Sets 16
2.3 Sequences 18
2.4 Induction 19
2.5 Background Reading 20
Ⅰ Untyped Systems 21
3 Untyped Arithmetic Expressions 23
3.1 Introduction 23
3.2 Syntax 26
3.3 Induction on Terms 29
3.4 Semantic Styles 32
3.5 Evaluation 34
3.6 Notes 43
4 An ML Implementation of Arithmetic Expressions 45
4.1 Syntax 46
4.2 Evaluation 47
4.3 The Rest of the Story 49
5 The Untyped Lambda-Calculus 51
5.1 Basics 52
5.2 Programming in the Lambda-Calculus 58
5.3 Formalities 68
5.4 Notes 73
6 Nameless Representation of Terms 75
6.1 Terms and Contexts 76
6.2 Shifting and Substitution 78
6.3 Evaluation 80
7 An ML Implementation of the Lambda-Calculus 83
7.1 Terms and Contexts 83
7.2 Shifting and Substitution 85
7.3 Evaluation 87
7.4 Notes 88
Ⅱ Simple Types 89
8 Typed Arithmetic Expressions 91
8.1 Types 91
8.2 The Typing Relation 92
8.3 Safety=Progress ＋ Preservation 95
9 Simply Typed Lambda-Calculus 99
9.1 Function Types 99
9.2 The Typing Relation 100
9.3 Properties of Typing 104
9.4 The Curry-Howard Correspondence 108
9.5 Erasure and Typability 109
9.6 Curry-Style vs.Church-Style 111
9.7 Notes 111
10 An ML Implementation of Simple Types 113
10.1 Contexts 113
10.2 Terms and Types 115
10.3 Typechecking 115
11 Simple Extensions 117
11.1 Base Types 117
11.2 The Unit Type 118
11.3 Derived Forms： Sequencing and Wildcards 119
11.4 Ascription 121
11.5 Let Bindings 124
11.6 Pairs 126
11.7 Tuples 128
11.8 Records 129
11.9 Sums 132
11.10 Variants 136
11.11 General Recursion 142
11.12 Lists 146
12 Normalization 149
12.1 Normalization for Simple Types 149
12.2 Notes 152
13 References 153
13.1 Introduction 153
13.2 Typing 159
13.3 Evaluation 159
13.4 Store Typings 162
13.5 Safety 165
13.6 Notes 170
14 Exceptions 171
14.1 Raising Exceptions 172
14.2 Handling Exceptions 173
14.3 Exceptions Carrying Values 175
Ⅲ Subtyping 179
15 Subtyping 181
15.1 Subsumption 181
15.2 The Subtype Relation 182
15.3 Properties of Subtyping and Typing 188
15.4 The Top and Bottom Types 191
15.5 Subtyping and Other Features 193
15.6 Coercion Semantics for Subtyping 200
15.7 Intersection and Union Types 206
15.8 Notes 207
16 Metatheory of Subtyping 209
16.1 Algorithmic Subtyping 210
16.2 Algorithmic Typing 213
16.3 Joins and Meets 218
16.4 Algorithmic Typing and the Bottom Type 220
17 An ML Implementation of Subtyping 221
17.1 Syntax 221
17.2 Subtyping 221
17.3 Typing 222
18 Case Study： Imperative Objects 225
18.1 What Is Object-Oriented Programming？ 225
18.2 Objects 228
18.3 Object Generators 229
18.4 Subtyping 229
18.5 Grouping Instance Variables 230
18.6 Simple Classes 231
18.7 Adding Instance Variables 233
18.8 Calling Superclass Methods 234
18.9 Classes with Self 234
18.10 Open Recursion through Self 235
18.11 Open Recursion and Evaluation Order 237
18.12 A More Efficient Implementation 241
18.13 Recap 244
18.14 Notes 245
19 Case Study： Featherweight Java 247
19.1 Introduction 247
19.2 Overview 249
19.3 Nominal and Structural Type Systems 251
19.4 Definitions 254
19.5 Properties 261
19.6 Encodings vs.Primitive Objects 262
19.7 Notes 263
Ⅳ Recursive Types 265
20 Recursive Types 267
20.1 Examples 268
20.2 Formalities 275
20.3 Subtyping 279
20.4 Notes 279
21 Metatheory of Recursive Types 281
21.1 Induction and Coinduction 282
21.2 Finite and Infinite Types 284
21.3 Subtyping 286
21.4 A Digression on Transitivity 288
21.5 Membership Checking 290
21.6 More Efficient Algorithms 295
21.7 Regular Trees 298
21.8 μ-Types 299
21.9 Counting Subexpressions 304
21.10 Digression： An Exponential Algorithm 309
21.11 Subtyping Iso-Recursive Types 311
21.12 Notes 312
V Polymorphism 315
22 Type Reconstruction 317
22.1 Type Variables and Substitutions 317
22.2 Two Views of Type Variables 319
22.3 Constraint-Based Typing 321
22.4 Unification 326
22.5 Principal Types 329
22.6 Implicit Type Annotations 330
22.7 Let-Polymorphism 331
22.8 Notes 336
23 Universal Types 339
23.1 Motivation 339
23.2 Varieties of Polymorphism 340
23.3 System F 341
23.4 Examples 344
23.5 Basic Properties 353
23.6 Erasure， Typability， and Type Reconstruction 354
23.7 Erasure and Evaluation Order 357
23.8 Fragments of System F 358
23.9 Parametricity 359
23.10 Impredicativity 360
23.11 Notes 361
24 Existential Types 363
24.1 Motivation 363
24.2 Data Abstraction with Existentials 368
24.3 Encoding Existentials 377
24.4 Notes 379
25 An ML Implementation of System F 381
25.1 Nameless Representation of Types 381
25.2 Type Shifting and Substitution 382
25.3 Terms 383
25.4 Evaluation 385
25.5 Typing 386
26 Bounded Quantification 389
26.1 Motivation 389
26.2 Definitions 391
26.3 Examples 396
26.4 Safety 400
26.5 Bounded Existential Types 406
26.6 Notes 408
27 Case Study： Imperative Objects， Redux 411
28 Metatheory of Bounded Quantification 417
28.1 Exposure 417
28.2 Minimal Typing 418
28.3 Subtyping in Kernel F〈： 421
28.4 Subtyping in Full F〈： 424
28.5 Undecidability of Full F〈： 427
28.6 Joins and Meets 432
28.7 Bounded Existentials 435
28.8 Bounded Quantification and the Bottom Type 436
Ⅵ Higher-Order Systems 437
29 Type Operators and Kinding 439
29.1 Intuitions 440
29.2 Definitions 445
30 Higher-Order Polymorphism 449
30.1 Definitions 449
30.2 Example 450
30.3 Properties 453
30.4 Fragments of Fω 461
30.5 Going Further： Dependent Types 462
31 Higher-Order Subtyping 467
31.1 Intuitions 467
31.2 Definitions 469
31.3 Properties 472
31.4 Notes 472
32 Case Study： Purely Functional Objects 475
32.1 Simple Objects 475
32.2 Subtyping 476
32.3 Bounded Quantification 477
32.4 Interface Types 479
32.5 Sending Messages to Objects 480
32.6 Simple Classes 481
32.7 Polymorphic Update 482
32.8 Adding Instance Variables 485
32.9 Classes with “Self” 486
32.10 Notes 488
Appendices 491
A Solutions to Selected Exercises 493
B Notational Conventions 565
B.1 Metavariable Names 565
B.2 Rule Naming Conventions 565
B.3 Naming and Subscripting Conventions 566
References 567
Index 605