Practical Foundations for Programming Languages 1.19

Version 1.19 of 10.03.2011......Page 1
Copyrightc 2011 by Robert Harper......Page 2
Preface......Page 3
Contents......Page 5
Judgements and Rules......Page 17
Syntactic Objects......Page 19
1.2 Abstract Syntax Trees......Page 20
1.3 Abstract Binding Trees......Page 23
1.4 Notes......Page 28
2.1 Judgements......Page 29
2.2 Inference Rules......Page 30
2.3 Derivations......Page 31
2.4 Rule Induction......Page 33
2.5 Iterated and Simultaneous Inductive De nitions......Page 35
2.6 De ning Functions by Rules......Page 36
2.7 Modes......Page 38
2.8 Notes......Page 39
3.1 Hypothetical Judgements......Page 41
3.2 Hypothetical Inductive De nitions......Page 45
3.3 General Judgements......Page 47
3.4 Generic Inductive De nitions......Page 48
3.5 Notes......Page 50
Levels of Syntax......Page 51
4.1 Lexical Structure......Page 53
4.2 Context-Free Grammars......Page 57
4.3 Grammatical Structure......Page 58
4.4 Ambiguity......Page 59
4.5 Notes......Page 61
5.1 Hierarchical and Binding Structure......Page 63
5.2 Parsing Into Abstract Syntax Trees......Page 65
5.3 Parsing Into Abstract Binding Trees......Page 67
5.4 Notes......Page 69
Statics and Dynamics......Page 71
6.1 Syntax......Page 73
6.2 Type System......Page 74
6.3 Structural Properties......Page 76
6.4 Notes......Page 78
7.1 Transition Systems......Page 79
7.2 Structural Dynamics......Page 80
7.3 Contextual Dynamics......Page 83
7.4 Equational Dynamics......Page 85
7.5 Notes......Page 88
Type Safety......Page 91
8.2 Progress......Page 92
8.3 Run-Time Errors......Page 94
8.4 Notes......Page 95
9.1 Evaluation Dynamics......Page 97
9.2 Relating Structural and Evaluation Dynamics......Page 98
9.3 Type Safety, Revisited......Page 99
9.4 Cost Dynamics......Page 101
9.5 Notes......Page 102
Function Types......Page 103
Function De nitions and Values......Page 105
10.1 First-Order Functions......Page 106
10.2 Higher-Order Functions......Page 107
10.3 Evaluation Dynamics and De nitional Equivalence......Page 109
10.4 Dynamic Scope......Page 111
10.5 Notes......Page 112
Godel'¨ s System T......Page 113
11.1 Statics......Page 114
11.2 Dynamics......Page 115
11.3 De nability......Page 116
11.4 Unde nability......Page 118
11.5 Notes......Page 120
Plotkin's PCF......Page 121
12.1 Statics......Page 123
12.2 Dynamics......Page 124
12.3 De nability......Page 126
12.4 Co-Natural Numbers......Page 128
12.5 Notes......Page 129
Finite Data Types......Page 131
Product Types......Page 133
13.1 Nullary and Binary Products......Page 134
13.2 Finite Products......Page 135
13.3 Primitive and Mutual Recursion......Page 137
13.4 Notes......Page 138
14.1 Binary and Nullary Sums......Page 139
14.2 Finite Sums......Page 141
14.3 Applications of Sum Types......Page 142
14.4 Notes......Page 145
Pattern Matching......Page 147
15.2 Statics......Page 148
15.3 Dynamics......Page 150
15.4 Exhaustiveness and Redundancy......Page 152
15.5 Notes......Page 157
16.1 Introduction......Page 159
16.3 Generic Extension......Page 160
16.4 Notes......Page 163
Infinite Data Types......Page 165
17.1 Motivating Examples......Page 167
17.2 Statics......Page 171
17.3 Dynamics......Page 172
17.4 Notes......Page 173
Recursive Types......Page 175
18.1 Solving Type Isomorphisms......Page 176
18.2 Recursive Data Structures......Page 177
18.3 Self-Reference......Page 179
18.4 Notes......Page 181
Dynamic Types......Page 183
19.1 The......Page 185
19.2 De nability......Page 187
19.3 Scott's Theorem......Page 190
19.4 Untyped Means Uni-Typed......Page 191
19.5 Notes......Page 193
20.1 Dynamically Typed PCF......Page 195
20.2 Variations and Extensions......Page 198
20.3 Critique of Dynamic Typing......Page 201
20.4 Notes......Page 202
21.1 A Hybrid Language......Page 205
21.2 Optimization of Dynamic Typing......Page 207
21.3 Static “Versus” Dynamic Typing......Page 209
21.4 Reduction to Recursive Types......Page 210
21.5 Notes......Page 211
Variable Types......Page 213
Girard's System F......Page 215
22.1 System F......Page 216
22.2 Polymorphic De nability......Page 219
22.3 Parametricity Overview......Page 221
22.4 Restricted Forms of Polymorphism......Page 222
22.5 Notes......Page 226
Abstract Types......Page 227
23.1 Existential Types......Page 228
23.2 Data Abstraction Via Existentials......Page 230
23.3 De nability of Existentials......Page 232
23.4 Representation Independence......Page 233
23.5 Notes......Page 235
Constructors and Kinds......Page 237
24.1 Statics......Page 238
24.2 Higher Kinds......Page 240
24.3 Hereditary Substitution......Page 242
24.4 Canonization......Page 245
24.5 Notes......Page 247
Subtyping......Page 249
Subtyping......Page 251
25.2 Varieties of Subtyping......Page 252
25.3 Variance......Page 255
25.4 Safety......Page 260
25.5 Notes......Page 262
Singleton Kinds......Page 263
26.1 Overview......Page 264
26.2 Singletons......Page 265
26.3 Dependent Kinds......Page 267
26.4 Higher Singletons......Page 271
26.5 Notes......Page 272
Classes and Methods......Page 273
27.1 The Dispatch Matrix......Page 275
27.2 Method-Based Organization......Page 277
27.3 Class-Based Organization......Page 279
27.4 Self-Reference......Page 281
27.5 Notes......Page 282
Inheritance......Page 283
28.1 Subclassing......Page 284
28.2 Notes......Page 287
Control Effects......Page 289
29.1 Machine De nition......Page 291
29.2 Safety......Page 293
29.3 Correctness of the Control Machine......Page 294
29.4 Notes......Page 298
30.1 Failures......Page 299
30.2 Exceptions......Page 301
30.3 Exception Type......Page 302
30.4 Encapsulation......Page 304
30.5 Notes......Page 306
31.1 Informal Overview......Page 307
31.2 Semantics of Continuations......Page 309
31.3 Coroutines......Page 311
31.4 Notes......Page 315
Types and Propositions......Page 317
Constructive Logic......Page 319
32.1 Constructive Semantics......Page 320
32.2 Constructive Logic......Page 321
32.3 Propositions as Types......Page 325
32.4 Notes......Page 326
Classical Logic......Page 327
33.1 Classical Logic......Page 328
33.2 Deriving Elimination Forms......Page 333
33.3 Proof Dynamics......Page 334
33.4 Law of the Excluded Middle......Page 336
33.5 The Double-Negation Translation......Page 338
33.6 Notes......Page 339
Symbols......Page 341
Symbols......Page 343
34.1 Symbol Declaration......Page 344
34.2 Symbolic References......Page 346
34.3 Notes......Page 349
35.1 Statics......Page 351
35.2 Dynamics......Page 352
35.3 Type Safety......Page 353
35.4 Some Subtleties......Page 354
35.5 Fluid References......Page 356
35.6 Notes......Page 358
Dynamic Classi cation......Page 359
36.1 Dynamic Classes......Page 360
36.2 Class References......Page 362
36.3 De nability of Dynamic Classes......Page 363
36.4 Classifying Secrets......Page 364
36.5 Notes......Page 365
Storage Effects......Page 367
37.1 Basic Commands......Page 369
37.2 Some Programming Idioms......Page 375
37.3 Typed Commands and Typed Assignables......Page 377
37.4 Capabilities......Page 380
37.5 References......Page 381
37.6 Aliasing......Page 382
37.7 Notes......Page 383
Mutable Data Structures......Page 385
38.1 Free Assignables......Page 386
38.2 Free References......Page 387
38.3 Safety......Page 388
38.4 Integrating Commands and Expressions......Page 390
38.5 Notes......Page 393
Laziness......Page 395
Lazy Evaluation......Page 397
39.1 Need Dynamics......Page 398
39.2 Safety......Page 402
39.3 Lazy Data Structures......Page 404
39.4 Suspensions......Page 405
39.5 Notes......Page 407
Polarization......Page 409
40.1 Positive and Negative Types......Page 410
40.2 Focusing......Page 411
40.3 Statics......Page 412
40.4 Dynamics......Page 414
40.5 Safety......Page 415
40.6 Polarization......Page 416
40.7 Notes......Page 417
Parallelism......Page 419
Nested Parallelism......Page 421
41.1 Binary Fork-Join......Page 422
41.2 Cost Dynamics......Page 425
41.3 Multiple Fork-Join......Page 428
41.4 Provably Ef cient Implementations......Page 430
41.5 Notes......Page 434
Futures and Speculation......Page 435
42.1 Futures......Page 436
42.2 Suspensions......Page 437
42.3 Parallel Dynamics......Page 438
42.4 Applications of Futures......Page 441
42.5 Notes......Page 443
Concurrency......Page 445
43.1 Actions and Events......Page 447
43.2 Interaction......Page 449
43.3 Replication......Page 451
43.4 Allocating Channels......Page 453
43.5 Communication......Page 456
43.6 Channel Passing......Page 459
43.7 Universality......Page 462
43.8 Notes......Page 464
44.1 Concurrent Algol......Page 465
44.2 Broadcast Communication......Page 468
44.3 Selective Communication......Page 470
44.4 Free Assignables as Processes......Page 474
44.5 Notes......Page 476
Distributed Algol......Page 477
45.1 Statics......Page 478
45.2 Dynamics......Page 480
45.3 Safety......Page 481
45.4 Situated Types......Page 482
45.5 Notes......Page 486
Modularity......Page 487
Components and Linking......Page 489
46.1 Simple Units and Linking......Page 490
46.2 Initialization and Effects......Page 491
46.3 Notes......Page 493
Type Abstractions and Type Classes......Page 495
47.1 Type Abstraction......Page 497
47.2 Type Classes......Page 499
47.3 A Module Language......Page 502
47.4 Firstand Second-Class......Page 507
47.5 Notes......Page 509
48.1 Hierarchy......Page 511
48.2 Parameterizaton......Page 515
48.3 Extending Modules with Hierarchies and Param-......Page 518
48.4 Notes......Page 521
Equivalence......Page 523
Equational Reasoning for T......Page 525
49.1 Observational Equivalence......Page 526
49.2 Logical Equivalence......Page 530
49.3 Logical and Observational Equivalence Coincide......Page 531
49.4 Some Laws of Equivalence......Page 534
49.5 Notes......Page 536
50.1 Observational Equivalence......Page 537
50.2 Logical Equivalence......Page 538
50.3 Logical and Observational Equivalence Coincide......Page 539
50.4 Compactness......Page 542
50.5 Co-Natural Numbers......Page 545
50.6 Notes......Page 547
51.1 Overview......Page 549
51.2 Observational Equivalence......Page 550
51.3 Logical Equivalence......Page 552
51.4 Parametricity Properties......Page 558
51.5 Representation Independence, Revisited......Page 561
51.6 Notes......Page 563
52.1 Process Calculus......Page 565
52.2 Strong Equivalence......Page 568
52.3 Weak Equivalence......Page 571
52.4 Notes......Page 573
Appendices......Page 575
Mathematical Preliminaries......Page 577
Bibliography......Page 579
Revision History......Page 589