Contents Preface to the Second Edition Preface to the First Edition I Judgments and Rules IEW 1 Abstract Syntax 3 1.1 Abstract Syntax Trees..... 4 1.2 Abstract Binding Trees 6 1.3 Notes.·.·.···· 10 2 Inductive Definitions 13 2.1 Judgments 13 2.2 Inference Rules 44444 14 2.3 Derivations....·.·. 15 2.4 Rule Induction..。.·...···· 16 2.5 Iterated and Simultaneous Inductive Definitions... 18 2.6 Defining Functions by Rules..,. 19 2.7 Notes.········ 20 3 Hypothetical and General Judgments 23 3.1 Hypothetical Judgments 23 3.1.1 Derivability ....... 23 3.1.2 Admissibility··..·...· 25 3.2 Hypothetical Inductive Definitions ... 26 3.3 General Judgments...············ 3.4 Generic Inductive Definitions 29 3.5 Notes...··············· 30
PREVIEW Contents Preface to the Second Edition iii Preface to the First Edition v I Judgments and Rules 1 1 Abstract Syntax 3 1.1 Abstract Syntax Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Abstract Binding Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2 Inductive Definitions 13 2.1 Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3 Derivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.4 Rule Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.5 Iterated and Simultaneous Inductive Definitions . . . . . . . . . . . . . . . . . . . . . 18 2.6 Defining Functions by Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.7 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3 Hypothetical and General Judgments 23 3.1 Hypothetical Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1.1 Derivability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.1.2 Admissibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2 Hypothetical Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.3 General Judgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3.4 Generic Inductive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
viii CONTENTS ⅡStatics and Dynamics 33 4 Statics 4.1 Syntax 36 4.2 Type System................. 4.3 Structural Properties.··········· 37 4.4 39 5 Dynamics 41 5.1 Transition Systems·.·.······· 41 5.2 Structural Dynamics 42 5.3 Contextual Dynamics....... 5.4 Equational Dynamics.·.·.·. % 5.5 Notes..········ 6 Type Safety 51 6.1 Preservation............ 52 6.2 Progress 6.3 Run-Time Errors....... 53 6.4 Notes......... 7 Evaluation Dynamics 57 7.1 Evaluation Dynamics.·.··· 7.2 Relating Structural and Evaluation Dynamics 58 7.3 Type Safety,Revisited............. 7.4 Cost Dynamics 7.5 Notes 61 III Total Functions 63 8 Function Definitions and Values 8.1 First-Order Functions. 65 8.2 Higher-Order Functions 8.3 Evaluation Dynamics and Definitional Equality 8.4 Dynamic Scope 0 8.5 Notes···············“ 71 9 System T of Higher-Order Recursion 7 9.1 Statics..··········· 73 9.2 Dynamics 9.3 Definability 9.4 Undefinability 77 9.5 Notes.······
PREVIEW viii CONTENTS II Statics and Dynamics 33 4 Statics 35 4.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 4.2 Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 4.3 Structural Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5 Dynamics 41 5.1 Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.2 Structural Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.3 Contextual Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 5.4 Equational Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 5.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6 Type Safety 51 6.1 Preservation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.2 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.3 Run-Time Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 6.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 7 Evaluation Dynamics 57 7.1 Evaluation Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 7.2 Relating Structural and Evaluation Dynamics . . . . . . . . . . . . . . . . . . . . . . . 58 7.3 Type Safety, Revisited . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 7.4 Cost Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 7.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 III Total Functions 63 8 Function Definitions and Values 65 8.1 First-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 8.2 Higher-Order Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 8.3 Evaluation Dynamics and Definitional Equality . . . . . . . . . . . . . . . . . . . . . 69 8.4 Dynamic Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 8.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 9 System T of Higher-Order Recursion 73 9.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 9.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 9.3 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 9.4 Undefinability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 9.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
CONTENTS 4 IV Finite Data Types 81 10 Product Types 83 10.1 Nullary and Binary Products 10.2 Finite Products 8 l0.3 Primitive Mutual Recursion·.,.....·····, 6 10.4 Notes...··················· 11 Sum Types 11.1 Nullary and Binary Sums 11.2 Finite Sums...··········· 11.3 Applications of Sum Types... 11.3.1 Void and Unit .. 11.3.2 Booleans....... 11.3.3 Enumerations .. 899922294 11.3.4 Options 11.4 Notes......... 95 V Types and Propositions 97 12 Constructive Logic 99 12.1 Constructive Semantics ····.100 12.2 Constructive Logic 100 12.2.1 Provability 101 12.2.2 Proof Terms 103 12.3 Proof Dynamics·. 104 12.4 Propositions as Types.·· 105 12.5 Notes...,. 105 13 Classical Logic 109 13.1 Classical Logic.··.· ··..110 13.1.1 Provability and Refutability ···.110 13.1.2 Proofs and Refutations 112 13.2 Deriving Elimination Forms 114 13.3 Proof Dynamics..···,. ..115 13.4 Law of the Excluded Middle 117 13.5 The Double-Negation Translation.. 118 13.6 Notes.........· 119 VI Infinite Data Types 121 14 Generic Programming 123 14.1 Introduction..... 123
PREVIEW CONTENTS ix IV Finite Data Types 81 10 Product Types 83 10.1 Nullary and Binary Products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 10.2 Finite Products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 10.3 Primitive Mutual Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 10.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 11 Sum Types 89 11.1 Nullary and Binary Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 11.2 Finite Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 11.3 Applications of Sum Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 11.3.1 Void and Unit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 11.3.2 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 11.3.3 Enumerations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 11.3.4 Options . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 11.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 V Types and Propositions 97 12 Constructive Logic 99 12.1 Constructive Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 12.2 Constructive Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 12.2.1 Provability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 12.2.2 Proof Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 12.3 Proof Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 12.4 Propositions as Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 12.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 13 Classical Logic 109 13.1 Classical Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 13.1.1 Provability and Refutability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 13.1.2 Proofs and Refutations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 13.2 Deriving Elimination Forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 13.3 Proof Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 13.4 Law of the Excluded Middle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 13.5 The Double-Negation Translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 13.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 VI Infinite Data Types 121 14 Generic Programming 123 14.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
CONTENTS 14.2 Polynomial Type Operators...··············· 123 l4.3 Positive Type Operators...··········.······ 126 127 15 Inductive and Coinductive Types 129 15.1 Motivating Examples.....·.·.···.··· 4 ·...129 15.2 Statics..............·········· 132 1521 Types..·················· 133 152.2 Expressions·············· 133 15.3 Dynamics.....············ 134 15.4 Solving Type Equations 135 15.5 Notes···················· 136 vII Variable Types 139 16 System F of Polymorphic Types 141 16.1 Polymorphic Abstraction... 142 16.2 Polymorphic Definability 145 16.2.1 Products and Sums 145 16.2.2 Natural Numbers. 146 16.3 Parametricity Overview 147 16.4 Notes....... 148 17 Abstract Types 151 17.1 Existential Types 151 17.1.1 Statics.. 152 17.1.2 Dynamics 152 17.13 Safety..· 153 17.2 Data Abstraction...... 153 17.3 Definability of Existential Types 155 17.4 Representation Independence 155 17.5 Notes....... 157 18 Higher Kinds 159 18.1 Constructors and Kinds 。。。 160 18.2 Constructor Equality 161 18.3 Expressions and Types 162 18.4 Notes◆.·········· 163 VIII Partiality and Recursive Types 165 19 System PCF of Recursive Functions 167 19.1 Statics....············· 169
PREVIEW x CONTENTS 14.2 Polynomial Type Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 14.3 Positive Type Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 14.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 15 Inductive and Coinductive Types 129 15.1 Motivating Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 15.2 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 15.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 15.2.2 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 15.3 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 15.4 Solving Type Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 15.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 VII Variable Types 139 16 System F of Polymorphic Types 141 16.1 Polymorphic Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142 16.2 Polymorphic Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 16.2.1 Products and Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 16.2.2 Natural Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 16.3 Parametricity Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 16.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 17 Abstract Types 151 17.1 Existential Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151 17.1.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 17.1.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 17.1.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 17.2 Data Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 17.3 Definability of Existential Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 17.4 Representation Independence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 17.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 18 Higher Kinds 159 18.1 Constructors and Kinds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160 18.2 Constructor Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 18.3 Expressions and Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 18.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163 VIII Partiality and Recursive Types 165 19 System PCF of Recursive Functions 167 19.1 Statics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
CONTENTS 女 19.2 Dynamics 170 l9.3 Definability.···.·········· 171 19.4 Finite and Infinite Data Structures 。。 173 19.5 Totality and Partiality.......... 174 19.6 Notes...·········· 175 20 System FPC of Recursive Types 177 20.1 Solving Type Equations 178 20.2 Inductive and Coinductive Types.···.··· 179 20.3Self-Reference................. 180 20.4 The Origin of State.·.·.·...···.··· 182 20.5 Notes..············· 183 IX Dynamic Types 185 21 The Untyped A-Calculus 187 21.1Theλ-Calculus 187 21.2 Definability ·····188 21.3 Scott's Theorem.·.·.· ····190 21.4 Untyped Means Uni-Typed 192 21.5 Notes.·········· 193 22 Dynamic Typing 195 22.1 Dynamically Typed PCF 196 22.2 Variations and Extensions. 199 22.3 Critique of Dynamic Typing.. 201 22.4 Notes..··... 44444 202 23 Hybrid Typing 205 23.1 A Hybrid Language.. .......205 23.2 Dynamic as Static Typing·..··· 207 23.3 Optimization of Dynamic Typing 208 23.4 Static Versus Dynamic Typing. 210 23.5 Notes . 211 X Subtyping 213 24 Structural Subtyping 215 24.1 Subsumption.. ..215 24.2 Varieties of Subtyping ....216 24.3 Variance 218 24.4 Dynamics and Safety 223 24.5 Notes...······ 224
PREVIEW CONTENTS xi 19.2 Dynamics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 19.3 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171 19.4 Finite and Infinite Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173 19.5 Totality and Partiality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174 19.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 20 System FPC of Recursive Types 177 20.1 Solving Type Equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178 20.2 Inductive and Coinductive Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179 20.3 Self-Reference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 180 20.4 The Origin of State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182 20.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183 IX Dynamic Types 185 21 The Untyped λ-Calculus 187 21.1 The λ-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 21.2 Definability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 21.3 Scott’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 21.4 Untyped Means Uni-Typed . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192 21.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 22 Dynamic Typing 195 22.1 Dynamically Typed PCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 22.2 Variations and Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199 22.3 Critique of Dynamic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 22.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 23 Hybrid Typing 205 23.1 A Hybrid Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 23.2 Dynamic as Static Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207 23.3 Optimization of Dynamic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208 23.4 Static Versus Dynamic Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210 23.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211 X Subtyping 213 24 Structural Subtyping 215 24.1 Subsumption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 24.2 Varieties of Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 216 24.3 Variance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218 24.4 Dynamics and Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223 24.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224