---

Preface . . . v
Prologue . . . 1

Review: Object-Oriented Features

1 Object Orientation . . . 7

1.1 Objects . . . 7
1.2 Reuse . . . 8
1.3 Classifying Features . . . 9

2 Class-Based Languages . . . 11

2.1 Classes and Objects . . . 11
2.2 Method Lookup . . . 13
2.3 Subclasses and Inheritance . . . 15
2.4 Subsumption and Dynamic Dispatch . . . 17
2.5 Type Information, Lost and Found . . . 19
2.6 Covariance, Contravariance, and Invariance . . . 20
2.7 Method Specialization . . . 22
2.8 Self Type Specialization . . . 23

3 Advanced Class-Based Features . . . 25

3.1 Object Types . . . 25
3.2 Distinguishing Subclassing from Subtyping . . . 27
3.3 Type Parameters . . . 28
3.4 Subclassing without Subtyping . . . 30
3.5 Object Protocols . . . 32

4 Object-Based Languages . . . 35

4.1 Objects without Classes . . . 35
4.2 Prototypes and Clones . . . 36
4.3 Inheritance by Embedding and by Delegation . . . 38
4.4 Embedding . . . 39
4.5 Delegation . . . 42
4.6 Embedding versus Delegation . . . 45
4.7 Dynamic Inheritance and Mode-Switching . . . 46
4.8 Traits: From Prototypes back to Classes? . . . 47
4.9 Types for Object-Based Languages . . . 49

5 Modeling Object-Oriented Languages . . . 51

5.1 Reduction to Basic Mechanisms . . . 51
5.2 The Role of Method Update . . . 52
5.3 The Scope of this Book . . . 53

Part I: Untyped and First-Order Calculi

6 Untyped Calculi . . . 57

6.1 Object Primitives . . . 57
6.2 The -Calculus . . . 60
6.3 Functions as Objects . . . 66
6.4 Fixpoints . . . 68
6.5 Examples . . . 69
6.6 Traits, Classes, and Inheritance . . . 73
6.7 Interpretations of Objects . . . 76

7 First-Order Calculi . . . 79

7.1 Formal Systems . . . 79
7.2 The Object Fragment . . . 80
7.3 Standard First-Order Fragments . . . 82
7.4 Examples . . . 84
7.5 Some Properties of Ob1 . . . 85
7.6 First-Order Equational Theories . . . 89
7.7 Functions and Fixpoints . . . 91

8 Subtyping . . . 93

8.1 Subtyping . . . 93
8.2 Examples . . . 95
8.3 Some Properties of Ob1<: . . . 95
8.4 First-Order Equational Theories with Subtyping . . . 98
8.5 Classes and Inheritance . . . 100
8.6 Objects versus Records . . . 106
8.7 Variance Annotations . . . 109

9 Recursion . . . 113

9.1 Recursion . . . 113
9.2 Recursion and Subsumption . . . 115
9.3 Some Properties of Ob1<: . . . 118
9.4 Examples . . . 121
9.5 The Shortcomings of First-Order Typing . . . 123
9.6 Towards the Type Self . . . 125
9.7 Dynamic Typing . . . 126

10 Untyped Imperative Calculi . . . 129

10.1 Syntax . . . 129
10.2 Fields . . . 130
10.3 Procedures . . . 131
10.4 Examples . . . 133
10.5 Operational Semantics . . . 135

11 First-Order Imperative Calculi . . . 141

11.1 Typing . . . 141
11.2 Examples of Typings . . . 142
11.3 Classes and Global Behavior Change . . . 144
11.4 Subject Reduction . . . 146

12 A First-Order Language . . . 153

12.1 Features . . . 153
12.2 Syntax . . . 154
12.3 Examples . . . 156
12.4 Typing . . . 159
12.5 Translation . . . 162

Part II: Second-Order Calculi

13 Second-Order Calculi . . . 169

13.1 The Universal Quantifier . . . 169
13.2 The Existential Quantifier . . . 173
13.3 Variance Properties . . . 177
13.4 Variant Product and Function Types, Encoded in Ob<: . . . 178
13.5 The Self Quantifier . . . 179

14 A Semantics . . . 185

14.1 The Untyped Universe . . . 185
14.2 Types in the Untyped Universe . . . 187
14.3 The Interpretation of Types and Typed Terms . . . 196

15 Definable Covariant Self Types . . . 201

15.1 -Objects . . . 201
15.2 Examples, with Typing . . . 205
15.3 Binary Methods and the Covariance Requirement . . . 208
15.4 Classes and Inheritance, with Self . . . 209
15.5 Updating from the Outside . . . 210
15.6 Recoup . . . 212
15.7 Objects with Structural Invariants . . . 215

16 Primitive Covariant Self Types . . . 221

16.1 Primitive Self Types and Structural Rules . . . 221
16.2 Objects with Structural Rules . . . 222
16.3 Quantifiers . . . 227
16.4 Subject Reduction . . . 229
16.5 Examples . . . 233
16.6 Classes and Inheritance, with Primitive Self . . . 237

17 Imperative Calculi with Self Types . . . 241

17.1 Syntax of Terms and Operational Semantics . . . 241
17.2 Typing with Self . . . 242
17.3 Quantifiers . . . 243
17.4 Examples . . . 245
17.5 Subject Reduction . . . 247

18 Interpretations of Object Calculi . . . 257

18.1 The Interpretation Problem . . . 257
18.2 Untyped Interpretations . . . 259
18.3 Typed Interpretations . . . 264

19 A Second-Order Language . . . 273

19.1 Features . . . 273
19.2 Syntax . . . 274
19.3 Examples . . . 276
19.4 Typing . . . 279
19.5 Translation . . . 282

Part III: Higher-Order Calculi

20 A Higher-Order Calculus . . . 287

20.1 Syntax of Ob<: . . . 287
20.2 Operational Semantics . . . 289
20.3 Typing . . . 290
20.4 Binary Methods . . . 294
20.5 Basic Properties of Ob<: . . . 298
20.6 Subject Reduction . . . 301

21 A Language with Matching . . . 305

21.1 Features . . . 305
21.2 Syntax . . . 306
21.3 Examples . . . 307
21.4 Typing . . . 311
21.5 Translation . . . 315

Epilogue . . . 325

Appendix: Rules and Proofs

A Fragments . . . 329

A.1 Simple-Objects Fragments . . . 329
A.2 Other Typing Fragments . . . 330
A.3 Other Equational Fragments . . . 333

B Systems . . . 337

B.1 The Ob1<: Calculus . . . 337
B.2 The F<:Calculus . . . 339
B.3 The Ob Calculus . . . 342

C Proofs . . . 347

C.1 Proof of the Variance Lemma from Section 13.3 . . . 347
C.2 Proof of the Variance Lemma from Section 16.4 . . . 351
C.3 Deriving the Rules for -Objects from Section 15.1.2 . . . 352
C.4 Denotational Soundness of Equational Rules . . . 354

List of Figures . . . 363
List of Tables . . . 365
List of Notations . . . 371
List of Languages . . . 381
Bibliography . . . 383
Index . . . 391