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..... 123PREVIEW 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