14.6 Continuations as a Language Feature . . . . . . . . . . . . . . . . . . 124
14.6.1 Presentation in the Language . . . . . . . . . . . . . . . . . . 125
14.6.2 Defining Generators . . . . . . . . . . . . . . . . . . . . . . 126
14.6.3 Defining Threads . . . . . . . . . . . . . . . . . . . . . . . . 127
14.6.4 Better Primitives for Web Programming . . . . . . . . . . . . 131
15 Checking Program Invariants Statically: Types 131
15.1 Types as Static Disciplines . . . . . . . . . . . . . . . . . . . . . . . 133
15.2 A Classical View of Types . . . . . . . . . . . . . . . . . . . . . . . 134
15.2.1 A Simple Type Checker . . . . . . . . . . . . . . . . . . . . 134
15.2.2 Type-Checking Conditionals . . . . . . . . . . . . . . . . . . 139
15.2.3 Recursion in Code . . . . . . . . . . . . . . . . . . . . . . . 139
15.2.4 Recursion in Data . . . . . . . . . . . . . . . . . . . . . . . . 142
15.2.5 Types, Time, and Space . . . . . . . . . . . . . . . . . . . . 144
15.2.6 Types and Mutation . . . . . . . . . . . . . . . . . . . . . . . 146
15.2.7 The Central Theorem: Type Soundness . . . . . . . . . . . . 147
15.3 Extensions to the Core . . . . . . . . . . . . . . . . . . . . . . . . . 148
15.3.1 Explicit Parametric Polymorphism . . . . . . . . . . . . . . . 148
15.3.2 Type Inference . . . . . . . . . . . . . . . . . . . . . . . . . 155
15.3.3 Union Types . . . . . . . . . . . . . . . . . . . . . . . . . . 164
15.3.4 Nominal Versus Structural Systems . . . . . . . . . . . . . . 170
15.3.5 Intersection Types . . . . . . . . . . . . . . . . . . . . . . . 171
15.3.6 Recursive Types . . . . . . . . . . . . . . . . . . . . . . . . 172
15.3.7 Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173
15.3.8 Object Types . . . . . . . . . . . . . . . . . . . . . . . . . . 176
16 Checking Program Invariants Dynamically: Contracts 179
16.1 Contracts as Predicates . . . . . . . . . . . . . . . . . . . . . . . . . 181
16.2 Tags, Types, and Observations on Values . . . . . . . . . . . . . . . . 182
16.3 Higher-Order Contracts . . . . . . . . . . . . . . . . . . . . . . . . . 183
16.4 Syntactic Convenience . . . . . . . . . . . . . . . . . . . . . . . . . 187
16.5 Extending to Compound Data Structures . . . . . . . . . . . . . . . . 188
16.6 More on Contracts and Observations . . . . . . . . . . . . . . . . . . 189
16.7 Contracts and Mutation . . . . . . . . . . . . . . . . . . . . . . . . . 189
16.8 Combining Contracts . . . . . . . . . . . . . . . . . . . . . . . . . . 190
16.9 Blame . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
17 Alternate Application Semantics 195
17.1 Lazy Application . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196
17.1.1 A Lazy Application Example . . . . . . . . . . . . . . . . . . 196
17.1.2 What Are Values? . . . . . . . . . . . . . . . . . . . . . . . 197
17.1.3 What Causes Evaluation? . . . . . . . . . . . . . . . . . . . 198
17.1.4 An Interpreter . . . . . . . . . . . . . . . . . . . . . . . . . . 199
17.1.5 Laziness and Mutation . . . . . . . . . . . . . . . . . . . . . 201
17.1.6 Caching Computation . . . . . . . . . . . . . . . . . . . . . 201
17.2 Reactive Application . . . . . . . . . . . . . . . . . . . . . . . . . . 201
5
评论0