A theory of objects

Cover......Page 1
Title Page......Page 5
Preface......Page 7
Contents......Page 11
Prologue......Page 17
Review: Object-Oriented Features......Page 21
1.1 Objects......Page 23
1.2 Reuse......Page 24
1.3 Classifying Features......Page 25
2.1 Classes and Objects......Page 27
2.2 Method Lookup......Page 29
2.3 Subclasses and Inheritance......Page 31
2.4 Subsumption and Dynamic Dispatch......Page 33
2.5 Type Information, Lost and Found......Page 35
2.6 Covariance, Contravariance, and Invariance......Page 36
2.7 Method Specialization......Page 38
2.8 Self Type Specialization......Page 39
3.1 Object Types......Page 41
3.2 Distinguishing Subclassing from Subtyping......Page 43
3.3 Type Parameters......Page 44
3.4 Subclassing without Subtyping......Page 46
3.5 Object Protocols......Page 48
4.1 Objects without Classes......Page 51
4.2 Prototypes and Clones......Page 52
4.3 Inheritance by Embedding and by Delegation......Page 54
4.4 Embedding......Page 55
4.5 Delegation......Page 58
4.6 Embedding versus Delegation......Page 61
4.7 Dynamic Inheritance and Mode-Switching......Page 62
4.8 Traits: From Prototypes back to Classes?......Page 63
4.9 Types for Object-Based Languages......Page 65
5.1 Reduction to Basic Mechanisms......Page 67
5.2 The Role of Method Update......Page 68
5.3 The Scope of this Book......Page 69
Part I: Untyped and First-Order Calculi......Page 71
6.1.1 The Primitives of the ζ-Calculus......Page 73
6.1.2 The Primitive Semantics of the ζ-Calculus......Page 74
6.1.3 Examples of Reductions......Page 75
6.2.1 Syntax......Page 76
6.2.2 Reduction......Page 77
6.2.3 Equations......Page 78
6.2.4 Operational Semantics......Page 79
6.2.6 Review of Notation......Page 81
6.3.1 λ-terms as Objects......Page 82
6.3.2 Default Arguments and Call-by-Keyword......Page 83
6.4 Fixpoints......Page 84
6.5.1 Movable Points......Page 85
6.5.3 Object-Oriented Natural Numbers......Page 86
6.5.4 A Calculator......Page 87
6.5.5 Storage Cells......Page 88
6.6.1 Representing Traits and Classes......Page 89
6.6.2 Representing Inheritance......Page 90
6.6.3 An Example......Page 91
6.7.1 The Self-Application Semantics......Page 92
6.7.2 The Recursive-Record Semantics......Page 93
6.7.3 Back to the Primitive Semantics......Page 94
7.1 Formal Systems......Page 95
7.2 The Object Fragment......Page 96
7.3 Standard First-Order Fragments......Page 98
7.4.2 Booleans......Page 100
7.5.1 Unique Types......Page 101
7.5.2 Subject Reduction......Page 102
7.6.1 Equational Rules......Page 105
7.6.2 Equality and self......Page 106
7.7 Functions and Fixpoints......Page 107
8.1 Subtyping......Page 109
8.3.1 Minimum Types......Page 111
8.3.2 Subject Reduction......Page 113
8.4 First-Order Equational Theories with Subtyping......Page 114
8.4.2 Equality, Subtyping, and self......Page 115
8.5.1 Representing Class Types and Inheritance......Page 116
8.5.2 Variations on Class Types......Page 117
8.5.3 An Example......Page 119
8.6.1 Records......Page 122
8.6.2 Method Extraction......Page 123
8.6.3 Elder......Page 124
8.7 Variance Annotations......Page 125
8.7.1 Object Types with Variance......Page 126
8.7.2 Encodings and Examples with Variance......Page 127
9.1 Recursion......Page 129
9.2 Recursion and Subsumption......Page 131
9.3.1 Minimum Types......Page 134
9.3.2 Subject Reduction......Page 136
9.4 Examples......Page 137
9.5 The Shortcomings of First-Order Typing......Page 139
9.6 Towards the Type Self......Page 141
9.7.1 Typecase......Page 142
9.7.2 Subject Reduction......Page 143
9.7.3 An Example......Page 144
10.1 Syntax......Page 145
10.2 Fields......Page 146
10.3 Procedures......Page 147
10.4.1 Booleans......Page 149
10.4.3 Iteration......Page 150
10.5 Operational Semantics......Page 151
10.5.1 Reduction Rules......Page 152
10.5.2 Examples of Reductions......Page 154
11.1 Typing......Page 157
11.2.1 Movable Points......Page 158
11.2.2 A Calculator......Page 159
11.3.1 Classes and Update......Page 160
11.3.2 Examples......Page 161
11.4.1 Typings with Stores......Page 162
11.4.2 Proof of Subject Reduction......Page 164
12.1 Features......Page 169
12.2 Syntax......Page 170
12.3 Examples......Page 172
12.4 Typing......Page 175
12.5 Translation......Page 178
Part II: Second-Order Calculi......Page 183
13.1.1 Parametric Polymorphism......Page 185
13.1.2 Bounded Parametric Polymorphism......Page 187
13.1.3 Structural Update......Page 188
13.2 The Existential Quantifier......Page 189
13.3 Variance Properties......Page 193
13.4 Variant Product and Function Types, Encoded in Ob_{<:}......Page 194
13.5 The Self Quantifier......Page 195
13.5.1 Defining the Self Quantifier......Page 196
13.5.2 Derived Rules for the Self Quantifier......Page 197
13.5.3 A Pure Second-Order Object Calculus......Page 199
14.1 The Untyped Universe......Page 201
14.2.2 Semantic Definitions for Type Constructors......Page 203
14.2.3 Inclusion and Subtyping......Page 205
14.2.4 Properties of Joins......Page 207
14.2.5 Metric Properties......Page 210
14.3.1 Interpreting Types......Page 212
14.3.2 Interpreting Typed Terms......Page 213
14.3.3 Soundness......Page 214
15.1.1 Defining ζ-Objects......Page 217
15.1.2 Derived Rules for ζ-Objects......Page 218
15.2.1 Movable Points......Page 221
15.2.4 Object-Oriented Natural Numbers......Page 222
15.2.5 A Calculator......Page 223
15.3 Binary Methods and the Covariance Requirement......Page 224
15.4 Classes and Inheritance, with Self......Page 225
15.5 Updating from the Outside......Page 226
15.6.1 The Recoup Method......Page 228
15.6.2 The Recoup Invariant......Page 229
15.6.3 The Recoup Method and Classes......Page 230
15.7.1 Towards Structural Rules......Page 231
15.7.2 Structural Objects......Page 232
15.7.3 Rules with Preliminary Structural Assumptions......Page 233
15.7.4 Rules with Structural Assumptions......Page 234
16.1 Primitive Self Types and Structural Rules......Page 237
16.2.1 Syntax of Types and Variance......Page 238
16.2.2 Syntax of Terms and Operational Semantics......Page 240
16.2.3 Judgments and Rules for Types......Page 241
16.2.4 Rules for Terms......Page 242
16.3 Quantifiers......Page 243
16.4 Subject Reduction......Page 245
16.5.1 Storage Cells......Page 249
16.5.2 Backup Methods......Page 251
16.5.4 Movable Points......Page 252
16.6.1 Classes......Page 253
16.6.3 Accessing Classes from Objects......Page 255
17.1.1 Syntax of Terms......Page 257
17.2 Typing with Self......Page 258
17.3 Quantifiers......Page 259
17.4.2 Alternative Forms of Method Update......Page 261
17.4.3 Protected Storage Cells......Page 262
17.5.1 Typings with Stores......Page 263
17.5.2 Proof of Subject Reduction......Page 265
18.1.1 Encoding Objects and Subtyping......Page 273
18.1.2 Features......Page 274
18.2.1 Self-Application......Page 275
18.2.2 Recursive Records......Page 276
18.2.3 State-Application......Page 277
18.2.4 Cyclic Records......Page 278
18.2.5 Split Methods......Page 279
18.3.1 Self-Application......Page 280
18.3.2 Recursive Records......Page 281
18.3.3 State-Application......Page 282
18.3.4 Cyclic Records......Page 283
18.3.5 Split Methods......Page 284
18.3.6 From Split Methods back to Self-Application, Imperatively......Page 287
18.3.7 Discussion......Page 288
19.1 Features......Page 289
19.2 Syntax......Page 290
19.3.1 Points......Page 292
19.3.2 Cells......Page 293
19.4 Typing......Page 295
19.5 Translation......Page 298
Part III: Higher-Order Calculi......Page 301
20.1 Syntax of Ob_{ω<:μ}......Page 303
20.2 Operational Semantics......Page 305
20.3 Typing......Page 306
20.4.1 Binary-Tree Objects......Page 310
20.4.2 Binary-Tree Classes......Page 311
20.5 Basic Properties of Ob_{ω<:μ}......Page 314
20.6 Subject Reduction......Page 317
21.1 Features......Page 321
21.2 Syntax......Page 322
21.3 Examples......Page 323
21.3.1 Binary Trees......Page 324
21.3.2 Cells......Page 325
21.3.3 Points......Page 326
21.4 Typing......Page 327
21.5.1 Types and Operators......Page 331
21.5.2 Towards a Translation......Page 332
21.5.3 Translation......Page 333
21.5.4 Soundness of the Translation......Page 335
Epilogue......Page 341
Appendix: Rules and Proofs......Page 343
A.1 Simple-Objects Fragments......Page 345
A.2 Other Typing Fragments......Page 346
A.3 Other Equational Fragments......Page 349
B.1 The Ob_{1<:} Calculus......Page 353
B.2 The F_{<:μ} Calculus......Page 355
B.3 The ζOb Calculus......Page 358
C.1 Proof of the Variance Lemma from Section 13.3......Page 363
C.2 Proof of the Variance Lemma from Section 16.4......Page 367
C.3 Deriving the Rules for ζ-Objects from Section 15.1.2......Page 368
C.4 Denotational Soundness of Equational Rules......Page 370
List of Figures......Page 379
List of Tables......Page 381
List of Notations......Page 387
List of Languages......Page 397
Bibliography......Page 399
Index......Page 407