A Theory of Objects (Monographs in Computer Science)

Procedural languages are generally well understood and their formal foundations cast in the forms of various lambda-calculi. For object-oriented languages however the situation is not as clear-cut. In this book the authors propose and develop a different approach by developing object calculi in which objects are treated as primitives. Using object calculi, the authors are able to explain both the semantics of objects and their typing rules and demonstrate how to develop all of the most important concepts of object-oriented programming languages: self, dynamic dispatch, classes, inheritance, protected and private methods, prototyping, subtyping, covariance and contravariance, and method specialization. Many researchers and graduate students will find this an important development of the underpinnings of object-oriented programming. 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_{