Types and Programming Languages

Cover......Page 1
Title Page......Page 5
Contents......Page 7
Preface......Page 15
1.1 Types in Computer Science......Page 25
1.2 What Type Systems Are Good For......Page 28
1.3 Type Systems and Language Design......Page 33
1.4 Capsule History......Page 34
1.5 Related Reading......Page 36
2.1 Sets, Relations, and Functions......Page 39
2.2 Ordered Sets......Page 40
2.3 Sequences......Page 42
2.4 Induction......Page 43
2.5 Background Reading......Page 44
Part I: Untyped Systems......Page 45
3.1 Introduction......Page 47
3.2 Syntax......Page 50
3.3 Induction on Terms......Page 53
3.4 Semantic Styles......Page 56
3.5 Evaluation......Page 58
3.6 Notes......Page 67
4 An ML Implementation of Arithmetic Expressions......Page 69
4.1 Syntax......Page 70
4.2 Evaluation......Page 71
4.3 The Rest of the Story......Page 73
5 The Untyped Lambda-Calculus......Page 75
5.1 Basics......Page 76
5.2 Programming in the Lambda-Calculus......Page 82
5.3 Formalities......Page 92
5.4 Notes......Page 97
6 Nameless Representation of Terms......Page 99
6.1 Terms and Contexts......Page 100
6.2 Shifting and Substitution......Page 102
6.3 Evaluation......Page 104
7.1 Terms and Contexts......Page 107
7.2 Shifting and Substitution......Page 109
7.3 Evaluation......Page 111
7.4 Notes......Page 112
Part II: Simple Types......Page 113
8.1 Types......Page 115
8.2 The Typing Relation......Page 116
8.3 Safety = Progress + Preservation......Page 119
9.1 Function Types......Page 123
9.2 The Typing Relation......Page 124
9.3 Properties of Typing......Page 128
9.4 The Curry-Howard Correspondence......Page 132
9.5 Erasure and Typability......Page 133
9.7 Notes......Page 135
10.1 Contexts......Page 137
10.3 Typechecking......Page 139
11.1 Base Types......Page 141
11.2 The Unit Type......Page 142
11.3 Derived Forms: Sequencing and Wildcards......Page 143
11.4 Ascription......Page 145
11.5 Let Bindings......Page 148
11.6 Pairs......Page 150
11.7 Tuples......Page 152
11.8 Records......Page 153
11.9 Sums......Page 156
11.10 Variants......Page 160
11.11 General Recursion......Page 166
11.12 Lists......Page 170
12.1 Normalization for Simple Types......Page 173
12.2 Notes......Page 176
13.1 Introduction......Page 177
13.3 Evaluation......Page 183
13.4 Store Typings......Page 186
13.5 Safety......Page 189
13.6 Notes......Page 194
14 Exceptions......Page 195
14.1 Raising Exceptions......Page 196
14.2 Handling Exceptions......Page 197
14.3 Exceptions Carrying Values......Page 199
Part III: Subtyping......Page 203
15.1 Subsumption......Page 205
15.2 The Subtype Relation......Page 206
15.3 Properties of Subtyping and Typing......Page 212
15.4 The Top and Bottom Types......Page 215
15.5 Subtyping and Other Features......Page 217
15.6 Coercion Semantics for Subtyping......Page 224
15.7 Intersection and Union Types......Page 230
15.8 Notes......Page 231
16 Metatheory of Subtyping......Page 233
16.1 Algorithmic Subtyping......Page 234
16.2 Algorithmic Typing......Page 237
16.3 Joins and Meets......Page 242
16.4 Algorithmic Typing and the Bottom Type......Page 244
17.2 Subtyping......Page 245
17.3 Typing......Page 246
18.1 What Is Object-Oriented Programming?......Page 249
18.2 Objects......Page 252
18.4 Subtyping......Page 253
18.5 Grouping Instance Variables......Page 254
18.6 Simple Classes......Page 255
18.7 Adding Instance Variables......Page 257
18.9 Classes with Self......Page 258
18.10 Open Recursion through Self......Page 259
18.11 Open Recursion and Evaluation Order......Page 261
18.12 A More Efficient Implementation......Page 265
18.13 Recap......Page 268
18.14 Notes......Page 269
19.1 Introduction......Page 271
19.2 Overview......Page 273
19.3 Nominal and Structural Type Systems......Page 275
19.4 Definitions......Page 278
19.5 Properties......Page 285
19.6 Encodings vs. Primitive Objects......Page 286
19.7 Notes......Page 287
Part IV: Recursive Types......Page 289
20 Recursive Types......Page 291
20.1 Examples......Page 292
20.2 Formalities......Page 299
20.4 Notes......Page 303
21 Metatheory of Recursive Types......Page 305
21.1 Induction and Coinduction......Page 306
21.2 Finite and Infinite Types......Page 308
21.3 Subtyping......Page 310
21.4 A Digression on Transitivity......Page 312
21.5 Membership Checking......Page 314
21.6 More Efficient Algorithms......Page 319
21.7 Regular Trees......Page 322
21.8 μ-Types......Page 323
21.9 Counting Subexpressions......Page 328
21.10 Digression: An Exponential Algorithm......Page 333
21.11 Subtyping Iso-Recursive Types......Page 335
21.12 Notes......Page 336
Part V: Polymorphism......Page 339
22.1 Type Variables and Substitutions......Page 341
22.2 Two Views of Type Variables......Page 343
22.3 Constraint-Based Typing......Page 345
22.4 Unification......Page 350
22.5 Principal Types......Page 353
22.6 Implicit Type Annotations......Page 354
22.7 Let-Polymorphism......Page 355
22.8 Notes......Page 360
23.1 Motivation......Page 363
23.2 Varieties of Polymorphism......Page 364
23.3 System F......Page 365
23.4 Examples......Page 368
23.5 Basic Properties......Page 377
23.6 Erasure, Typability, and Type Reconstruction......Page 378
23.7 Erasure and Evaluation Order......Page 381
23.8 Fragments of System F......Page 382
23.9 Parametricity......Page 383
23.10 Impredicativity......Page 384
23.11 Notes......Page 385
24.1 Motivation......Page 387
24.2 Data Abstraction with Existentials......Page 392
24.3 Encoding Existentials......Page 401
24.4 Notes......Page 403
25.1 Nameless Representation of Types......Page 405
25.2 Type Shifting and Substitution......Page 406
25.3 Terms......Page 407
25.4 Evaluation......Page 409
25.5 Typing......Page 410
26.1 Motivation......Page 413
26.2 Definitions......Page 415
26.3 Examples......Page 420
26.4 Safety......Page 424
26.5 Bounded Existential Types......Page 430
26.6 Notes......Page 432
27 Case Study: Imperative Objects, Redux......Page 435
28.1 Exposure......Page 441
28.2 Minimal Typing......Page 442
28.3 Subtyping in Kernel F_{<:}......Page 445
28.4 Subtyping in Full F_{<:}......Page 448
28.5 Undecidability of Full F_{<:}......Page 451
28.6 Joins and Meets......Page 456
28.7 Bounded Existentials......Page 459
28.8 Bounded Quantification and the Bottom Type......Page 460
Part VI: Higher-Order Systems......Page 461
29 Type Operators and Kinding......Page 463
29.1 Intuitions......Page 464
29.2 Definitions......Page 469
30.1 Definitions......Page 473
30.2 Example......Page 474
30.3 Properties......Page 477
30.4 Fragments of F_ω......Page 485
30.5 Going Further: Dependent Types......Page 486
31.1 Intuitions......Page 491
31.2 Definitions......Page 493
31.4 Notes......Page 496
32.1 Simple Objects......Page 499
32.2 Subtyping......Page 500
32.3 Bounded Quantification......Page 501
32.4 Interface Types......Page 503
32.5 Sending Messages to Objects......Page 504
32.6 Simple Classes......Page 505
32.7 Polymorphic Update......Page 506
32.8 Adding Instance Variables......Page 509
32.9 Classes with “Self”......Page 510
32.10 Notes......Page 512
Appendices......Page 515
3......Page 517
5......Page 523
6......Page 527
8......Page 528
9......Page 529
11......Page 531
12......Page 536
13......Page 537
14......Page 540
15......Page 541
16......Page 544
17......Page 550
18......Page 552
19......Page 554
20......Page 558
21......Page 561
22......Page 566
23......Page 570
24......Page 576
26......Page 578
27......Page 581
28......Page 582
29......Page 583
30......Page 584
31......Page 586
32......Page 587
B.2 Rule Naming Conventions......Page 589
B.3 Naming and Subscripting Conventions......Page 590
A......Page 591
B......Page 593
C......Page 596
D......Page 600
F......Page 602
G......Page 603
H......Page 605
J......Page 608
K......Page 609
L......Page 610
M......Page 612
N......Page 615
P......Page 616
R......Page 619
S......Page 622
T......Page 623
U......Page 624
W......Page 625
X......Page 626
Z......Page 627
Index......Page 629