You are previewing Practical Foundations for Programming Languages.
O'Reilly logo
Practical Foundations for Programming Languages

Book Description

Types are the central organizing principle of the theory of programming languages. In this innovative book, Professor Robert Harper offers a fresh perspective on the fundamentals of these languages through the use of type theory. Whereas most textbooks on the subject emphasize taxonomy, Harper instead emphasizes genetics, examining the building blocks from which all programming languages are constructed. Language features are manifestations of type structure. The syntax of a language is governed by the constructs that define its types, and its semantics is determined by the interactions among those constructs. The soundness of a language design - the absence of ill-defined programs - follows naturally. Professor Harper's presentation is simultaneously rigorous and intuitive, relying on elementary mathematics. The framework he outlines scales easily to a rich variety of language concepts and is directly applicable to their implementation. The result is a lucid introduction to programming theory that is both accessible and practical.

Table of Contents

  1. Cover
  2. Practical Foundations for Programming Languages
  3. Title
  4. Copy Right
  5. Contents
  6. Preface
  7. Part I Judgments and Rules
    1. 1 Syntactic Objects
      1. 1.1 Abstract Syntax Trees
      2. 1.2 Abstract Binding Trees
      3. 1.3 Notes
    2. 2 Inductive Definitions
      1. 2.1 Judgments
      2. 2.2 Inference Rules
      3. 2.3 Derivations
      4. 2.4 Rule Induction
      5. 2.5 Iterated and Simultaneous Inductive Definitions
      6. 2.6 Defining Functions by Rules
      7. 2.7 Modes
      8. 2.8 Notes
    3. 3 Hypothetical and General Judgments
      1. 3.1 Hypothetical Judgments
        1. 3.1.1 Derivability
        2. 3.1.2 Admissibility
      2. 3.2 Hypothetical Inductive Definitions
      3. 3.3 General Judgments
      4. 3.4 Generic Inductive Definitions
      5. 3.5 Notes
  8. Part II Statics and Dynamics
    1. 4 Statics
      1. 4.1 Syntax
      2. 4.2 Type System
      3. 4.3 Structural Properties
      4. 4.4 Notes
    2. 5 Dynamics
      1. 5.1 Transition Systems
      2. 5.2 Structural Dynamics
      3. 5.3 Contextual Dynamics
      4. 5.4 Equational Dynamics
      5. 5.5 Notes
    3. 6 Type Safety
      1. 6.1 Preservation
      2. 6.2 Progress
      3. 6.3 Run-Time Errors
      4. 6.4 Notes
    4. 7 Evaluation Dynamics
      1. 7.1 Evaluation Dynamics
      2. 7.2 Relating Structural and Evaluation Dynamics
      3. 7.3 Type Safety, Revisited
      4. 7.4 Cost Dynamics
      5. 7.5 Notes
  9. Part III Function Types
    1. 8 Function Definitions and Values
      1. 8.1 First-Order Functions
      2. 8.2 Higher-Order Functions
      3. 8.3 Evaluation Dynamics and Definitional Equality
      4. 8.4 Dynamic Scope
      5. 8.5 Notes
    2. 9 Gödel’s T
      1. 9.1 Statics
      2. 9.2 Dynamics
      3. 9.3 Definability
      4. 9.4 Undefinability
      5. 9.5 Notes
    3. 10 Plotkin’s PCF
      1. 10.1 Statics
      2. 10.2 Dynamics
      3. 10.3 Definability
      4. 10.4 Notes
  10. Part IV Finite Data Types
    1. 11 Product Types
      1. 11.1 Nullary and Binary Products
      2. 11.2 Finite Products
      3. 11.3 Primitive and Mutual Recursions
      4. 11.4 Notes
    2. 12 Sum Types
      1. 12.1 Nullary and Binary Sums
      2. 12.2 Finite Sums
      3. 12.3 Applications of Sum Types
        1. 12.3.1 Void and Unit
        2. 12.3.2 Booleans
        3. 12.3.3 Enumerations
        4. 12.3.4 Options
      4. 12.4 Notes
    3. 13 Pattern Matching
      1. 13.1 A Pattern Language
      2. 13.2 Statics
      3. 13.3 Dynamics
      4. 13.4 Exhaustiveness and Redundancy
        1. 13.4.1 Match Constraints
        2. 13.4.2 Enforcing Exhaustiveness and Redundancy
        3. 13.4.3 Checking Exhaustiveness and Redundancy
      5. 13.5 Notes
    4. 14 Generic Programming
      1. 14.1 Introduction
      2. 14.2 Type Operators
      3. 14.3 Generic Extension
      4. 14.4 Notes
  11. Part V Infinite Data Types
    1. 15 Inductive and Coinductive Types
      1. 15.1 Motivating Examples
      2. 15.2 Statics
        1. 15.2.1 Types
        2. 15.2.2 Expressions
      3. 15.3 Dynamics
      4. 15.4 Notes
    2. 16 Recursive Types
      1. 16.1 Solving Type Isomorphisms
      2. 16.2 Recursive Data Structures
      3. 16.3 Self-Reference
      4. 16.4 The Origin of State
      5. 16.5 Notes
  12. Part VI Dynamic Types
    1. 17 The Untyped λ-Calculus
      1. 17.1 The λ-Calculus
      2. 17.2 Definability
      3. 17.3 Scott’s Theorem
      4. 17.4 Untyped Means Unityped
      5. 17.5 Notes
    2. 18 Dynamic Typing
      1. 18.1 Dynamically Typed PCF
      2. 18.2 Variations and Extensions
      3. 18.3 Critique of Dynamic Typing
      4. 18.4 Notes
    3. 19 Hybrid Typing
      1. 19.1 A Hybrid Language
      2. 19.2 Dynamics as Static Typing
      3. 19.3 Optimization of Dynamic Typing
      4. 19.4 Static Versus Dynamic Typing
      5. 19.5 Notes
  13. Part VII Variable Types
    1. 20 Girard’s System F
      1. 20.1 System F
      2. 20.2 Polymorphic Definability
        1. 20.2.1 Products and Sums
        2. 20.2.2 Natural Numbers
      3. 20.3 Parametricity Overview
      4. 20.4 Restricted Forms of Polymorphism
        1. 20.4.1 Predicative Fragment
        2. 20.4.2 Prenex Fragment
        3. 20.4.3 Rank-Restricted Fragments
      5. 20.5 Notes
    2. 21 Abstract Types
      1. 21.1 Existential Types
        1. 21.1.1 Statics
        2. 21.1.2 Dynamics
        3. 21.1.3 Safety
      2. 21.2 Data Abstraction Via Existentials
      3. 21.3 Definability of Existentials
      4. 21.4 Representation Independence
      5. 21.5 Notes
    3. 22 Constructors and Kinds
      1. 22.1 Statics
      2. 22.2 Higher Kinds
      3. 22.3 Canonizing Substitution
      4. 22.4 Canonization
      5. 22.5 Notes
  14. Part VIII Subtyping
    1. 23 Subtyping
      1. 23.1 Subsumption
      2. 23.2 Varieties of Subtyping
        1. 23.2.1 Numeric Types
        2. 23.2.2 Product Types
        3. 23.2.3 Sum Types
      3. 23.3 Variance
        1. 23.3.1 Product and Sum Types
        2. 23.3.2 Function Types
        3. 23.3.3 Quantified Types
        4. 23.3.4 Recursive Types
      4. 23.4 Safety
      5. 23.5 Notes
    2. 24 Singleton Kinds
      1. 24.1 Overview
      2. 24.2 Singletons
      3. 24.3 Dependent Kinds
      4. 24.4 Higher Singletons
      5. 24.5 Notes
  15. Part IX Classes and Methods
    1. 25 Dynamic Dispatch
      1. 25.1 The Dispatch Matrix
      2. 25.2 Class-Based Organization
      3. 25.3 Method-Based Organization
      4. 25.4 Self-Reference
      5. 25.5 Notes
    2. 26 Inheritance
      1. 26.1 Class and Method Extension
      2. 26.2 Class-Based Inheritance
      3. 26.3 Method-Based Inheritance
      4. 26.4 Notes
  16. Part X Exceptions and Continuations
    1. 27 Control Stacks
      1. 27.1 Machine Definition
      2. 27.2 Safety
      3. 27.3 Correctness of the Control Machine
        1. 27.3.1 Completeness
        2. 27.3.2 Soundness
      4. 27.4 Notes
    2. 28 Exceptions
      1. 28.1 Failures
      2. 28.2 Exceptions
      3. 28.3 Exception Type
      4. 28.4 Encapsulation of Exceptions
      5. 28.5 Notes
    3. 29 Continuations
      1. 29.1 Informal Overview
      2. 29.2 Semantics of Continuations
      3. 29.3 Coroutines
      4. 29.4 Notes
  17. Part XI Types and Propositions
    1. 30 Constructive Logic
      1. 30.1 Constructive Semantics
      2. 30.2 Constructive Logic
        1. 30.2.1 Provability
        2. 30.2.2 Proof Terms
      3. 30.3 Proof Dynamics
      4. 30.4 Propositions as Types
      5. 30.5 Notes
    2. 31 Classical Logic
      1. 31.1 Classical Logic
        1. 31.1.1 Provability and Refutability
        2. 31.1.2 Proofs and Refutations
      2. 31.2 Deriving Elimination Forms
      3. 31.3 Proof Dynamics
      4. 31.4 Law of the Excluded Middle
      5. 31.5 The Double-Negation Translation
      6. 31.6 Notes
  18. Part XII Symbols
    1. 32 Symbols
      1. 32.1 Symbol Declaration
        1. 32.1.1 Scoped Dynamics
        2. 32.1.2 Scope-Free Dynamics
      2. 32.2 Symbolic References
        1. 32.2.1 Statics
        2. 32.2.2 Dynamics
        3. 32.2.3 Safety
      3. 32.3 Notes
    2. 33 Fluid Binding
      1. 33.1 Statics
      2. 33.2 Dynamics
      3. 33.3 Type Safety
      4. 33.4 Some Subtleties
      5. 33.5 Fluid References
      6. 33.6 Notes
    3. 34 Dynamic Classification
      1. 34.1 Dynamic Classes
        1. 34.1.1 Statics
        2. 34.1.2 Dynamics
        3. 34.1.3 Safety
      2. 34.2 Class References
      3. 34.3 Definability of Dynamic Classes
      4. 34.4 Classifying Secrets
      5. 34.5 Notes
  19. Part XIII State
    1. 35 Modernized Algol
      1. 35.1 Basic Commands
        1. 35.1.1 Statics
        2. 35.1.2 Dynamics
        3. 35.1.3 Safety
      2. 35.2 Some Programming Idioms
      3. 35.3 Typed Commands and Typed Assignables
      4. 35.4 Notes
    2. 36 Assignable References
      1. 36.1 Capabilities
      2. 36.2 Scoped Assignables
      3. 36.3 Free Assignables
      4. 36.4 Safety for Free Assignables
      5. 36.5 Benign Effects
      6. 36.6 Notes
  20. Part XIV Laziness
    1. 37 Lazy Evaluation
      1. 37.1 By-Need Dynamics
      2. 37.2 Safety
      3. 37.3 Lazy Data Structures
      4. 37.4 Suspensions
      5. 37.5 Notes
    2. 38 Polarization
      1. 38.1 Positive and Negative Types
      2. 38.2 Focusing
      3. 38.3 Statics
      4. 38.4 Dynamics
      5. 38.5 Safety
      6. 38.6 Notes
  21. Part XV Parallelism
    1. 39 Nested Parallelism
      1. 39.1 Binary Fork–Join
      2. 39.2 Cost Dynamics
      3. 39.3 Multiple Fork–Join
      4. 39.4 Provably Efficient Implementations
      5. 39.5 Notes
    2. 40 Futures and Speculations
      1. 40.1 Futures
        1. 40.1.1 Statics
        2. 40.1.2 Sequential Dynamics
      2. 40.2 Speculations
        1. 40.2.1 Statics
        2. 40.2.2 Sequential Dynamics
      3. 40.3 Parallel Dynamics
      4. 40.4 Applications of Futures
      5. 40.5 Notes
  22. Part XVI Concurrency
    1. 41 Process Calculus
      1. 41.1 Actions and Events
      2. 41.2 Interaction
      3. 41.3 Replication
      4. 41.4 Allocating Channels
      5. 41.5 Communication
      6. 41.6 Channel Passing
      7. 41.7 Universality
      8. 41.8 Notes
    2. 42 Concurrent Algol
      1. 42.1 Concurrent Algol
      2. 42.2 Broadcast Communication
      3. 42.3 Selective Communication
      4. 42.4 Free Assignables as Processes
      5. 42.5 Notes
    3. 43 Distributed Algol
      1. 43.1 Statics
      2. 43.2 Dynamics
      3. 43.3 Safety
      4. 43.4 Situated Types
      5. 43.5 Notes
  23. Part XVII Modularity
    1. 44 Components and Linking
      1. 44.1 Simple Units and Linking
      2. 44.2 Initialization and Effects
      3. 44.3 Notes
    2. 45 Type Abstractions and Type Classes
      1. 45.1 Type Abstraction
      2. 45.2 Type Classes
      3. 45.3 A Module Language
      4. 45.4 First and Second Class
      5. 45.5 Notes
    3. 46 Hierarchy and Parameterization
      1. 46.1 Hierarchy
      2. 46.2 Parameterization
      3. 46.3 Extending Modules With Hierarchies and Parameterization
      4. 46.4 Applicative Functors
      5. 46.5 Notes
  24. Part XVIII Equational Reasoning
    1. 47 Equational Reasoning for T
      1. 47.1 Observational Equivalence
      2. 47.2 Logical Equivalence
      3. 47.3 Logical and Observational Equivalences Coincide
      4. 47.4 Some Laws of Equality
        1. 47.4.1 General Laws
        2. 47.4.2 Equality Laws
        3. 47.4.3 Induction Law
      5. 47.5 Notes
    2. 48 Equational Reasoning for PCF
      1. 48.1 Observational Equivalence
      2. 48.2 Logical Equivalence
      3. 48.3 Logical and Observational Equivalences Coincide
      4. 48.4 Compactness
      5. 48.5 Conatural Numbers
      6. 48.6 Notes
    3. 49 Parametricity
      1. 49.1 Overview
      2. 49.2 Observational Equivalence
      3. 49.3 Logical Equivalence
      4. 49.4 Parametricity Properties
      5. 49.5 Representation Independence, Revisited
      6. 49.6 Notes
    4. 50 Process Equivalence
      1. 50.1 Process Calculus
      2. 50.2 Strong Equivalence
      3. 50.3 Weak Equivalence
      4. 50.4 Notes
  25. Part XIX Appendix
    1. Appendix: Finite Sets and Finite Functions
    2. Bibliography
    3. Index