《编译原理与技术》课程教学资源（教材书籍）Practical Foundations for Programming Languages（SECOND EDITION，Robert Harper Carnegie Mellon University）.pdf_P11-P15

PREVIEW xii CONTENTS 25 Behavioral Typing 227 25.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228 25.2 Boolean Blindness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234 25.3 Refinement Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236 25.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 XI Dynamic Dispatch 241 26 Classes and Methods 243 26.1 The Dispatch Matrix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244 26.2 Class-Based Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246 26.3 Method-Based Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 26.4 Self-Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248 26.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 250 27 Inheritance 253 27.1 Class and Method Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253 27.2 Class-Based Inheritance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 254 27.3 Method-Based Inheritance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255 27.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256 XII Control Flow 259 28 Control Stacks 261 28.1 Machine Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261 28.2 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263 28.3 Correctness of the Stack Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 264 28.3.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 265 28.3.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 266 28.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267 29 Exceptions 269 29.1 Failures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 269 29.2 Exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271 29.3 Exception Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 272 29.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273 30 Continuations 275 30.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275 30.2 Continuation Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 277 30.3 Coroutines from Continuations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278 30.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 281

PREVIEW CONTENTS xiii XIII Symbolic Data 283 31 Symbols 285 31.1 Symbol Declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 286 31.1.1 Scoped Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 286 31.1.2 Scope-Free Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287 31.2 Symbol References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 288 31.2.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 288 31.2.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 31.2.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 31.3 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 290 32 Fluid Binding 293 32.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293 32.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 294 32.3 Type Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 295 32.4 Some Subtleties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 296 32.5 Fluid References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 297 32.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 299 33 Dynamic Classification 301 33.1 Dynamic Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301 33.1.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301 33.1.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 302 33.1.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303 33.2 Class References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303 33.3 Definability of Dynamic Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304 33.4 Applications of Dynamic Classification . . . . . . . . . . . . . . . . . . . . . . . . . . 305 33.4.1 Classifying Secrets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 305 33.4.2 Exception Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 306 33.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 306 XIV Mutable State 309 34 Modernized Algol 311 34.1 Basic Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311 34.1.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312 34.1.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313 34.1.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315 34.2 Some Programming Idioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 316 34.3 Typed Commands and Typed Assignables . . . . . . . . . . . . . . . . . . . . . . . . . 317 34.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319

PREVIEW xiv CONTENTS 35 Assignable References 323 35.1 Capabilities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323 35.2 Scoped Assignables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 324 35.3 Free Assignables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 326 35.4 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 328 35.5 Benign Effects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 330 35.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 332 36 Lazy Evaluation 335 36.1 PCF By-Need . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 336 36.2 Safety of PCF By-Need . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 338 36.3 FPC By-Need . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 340 36.4 Suspension Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341 36.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343 XV Parallelism 345 37 Nested Parallelism 347 37.1 Binary Fork-Join . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 347 37.2 Cost Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 350 37.3 Multiple Fork-Join . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 353 37.4 Bounded Implementations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 355 37.5 Scheduling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 359 37.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 360 38 Futures and Speculations 363 38.1 Futures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 38.1.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 38.1.2 Sequential Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 364 38.2 Speculations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 365 38.2.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 365 38.2.2 Sequential Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 365 38.3 Parallel Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 366 38.4 Pipelining With Futures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368 38.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 369 XVI Concurrency and Distribution 371 39 Process Calculus 373 39.1 Actions and Events . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 373 39.2 Interaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 375 39.3 Replication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377

PREVIEW CONTENTS xv 39.4 Allocating Channels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 378 39.5 Communication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 380 39.6 Channel Passing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 383 39.7 Universality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 385 39.8 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 386 40 Concurrent Algol 389 40.1 Concurrent Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 390 40.2 Broadcast Communication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 392 40.3 Selective Communication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 394 40.4 Free Assignables as Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 396 40.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 398 41 Distributed Algol 399 41.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399 41.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 402 41.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 404 41.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 404 XVII Modularity 407 42 Modularity and Linking 409 42.1 Simple Units and Linking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 409 42.2 Initialization and Effects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410 42.3 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 412 43 Singleton Kinds and Subkinding 413 43.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 414 43.2 Singletons . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 414 43.3 Dependent Kinds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 416 43.4 Higher Singletons . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419 43.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 44 Type Abstractions and Type Classes 423 44.1 Type Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 424 44.2 Type Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425 44.3 A Module Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 428 44.4 First- and Second-Class . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 44.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 433

PREVIEW xvi CONTENTS 45 Hierarchy and Parameterization 435 45.1 Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 435 45.2 Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 438 45.3 Hierarchy and Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 440 45.4 Applicative Functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442 45.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 443 XVIII Equational Reasoning 445 46 Equality for System T 447 46.1 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 447 46.2 Logical Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 450 46.3 Logical and Observational Equivalence Coincide . . . . . . . . . . . . . . . . . . . . . 452 46.4 Some Laws of Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 46.4.1 General Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 46.4.2 Equality Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 455 46.4.3 Induction Law . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 455 46.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 456 47 Equality for System PCF 457 47.1 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 457 47.2 Logical Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 47.3 Logical and Observational Equivalence Coincide . . . . . . . . . . . . . . . . . . . . . 458 47.4 Compactness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 461 47.5 Lazy Natural Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 464 47.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465 48 Parametricity 467 48.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 467 48.2 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 468 48.3 Logical Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 469 48.4 Parametricity Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 474 48.5 Representation Independence, Revisited . . . . . . . . . . . . . . . . . . . . . . . . . . 477 48.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 478 49 Process Equivalence 479 49.1 Process Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 479 49.2 Strong Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 481 49.3 Weak Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 484 49.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 485