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....············· 169PREVIEW 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