Object-Oriented Programming A Unified Foundation

by Luea Cardelli Ever since Strachey's work in the 1960's, polymorphism has been classified into the parametric and overloading varieties. Parametric polymorphism has been the subject of extensive study for over two decades. Overloading, on the other hand, has often been considered too ad hoc to deserve much attention even though it has been, in some form, an ingredient of virtually every programming lan­ guage (much more so than parametric polymorphism). With the introduction of object-oriented languages, and in particular with multiple-dispatch object-oriented languages, overloading has become less of a programming convenience and more of a fundamental feature in need of proper explanation. This book provides a compelling framework for the study of run-time over­ loading and of its interactions with subtyping and with parametric polymorphism. The book also describes applications to object-oriented programming. This new framework is motivated by the relatively recent spread of programming languages that are entirely based on run-time overloading; this fact probably explains why this subject was not investigated earlier. Once properly understood, overloading reveals itself relevant also to the study of older and more conventional (single­ dispatch) object-oriented languages, clarifying delicate issues of covariance and contravariance of method types, and of run-time type analysis. In the final chapters, a synthesis is made between parametric and overloading polymorphism.

I Introduction.- 1 Background and notation.- 1.1 ?-notation.- 1.1.1 The origins of ?-calculus.- 1.1.2 Datatypes.- 1.2 Simply-typed ?-calculus.- 1.2.1 Reduction.- 1.2.2 Typing.- 1.2.3 Properties.- 1.2.4 Fixed point operators.- 1.3 Subtyping.- 1.3.1 The ??-calculus.- 1.3.2 Records.- 1.3.3 Cartesian products.- 1.3.4 Recursive types.- 1.4 Further definitions.- 1.4.1 Algebra.- 1.4.2 Term rewriting systems.- 1.4.3 Logic.- 2 A quick overview.- 2.1 Introduction.- 2.2 Object-oriented programming.- 2.3 The ?&-calculus.- 2.4 Covariance and contravariance.- 2.5 Strong normalization.- 2.6 Three variations on the theme.- 2.7 Interpretation of object-oriented languages.- 2.8 Imperative features.- 2.9 Semantics.- 2.10 Second-order.- 2.11 Second order overloading.- 2.12 F?& and object-oriented programming.- 2.13 Conclusion.- II Simple typing.- 3 Object-oriented programming.- 3.1 A kernel object-oriented language.- 3.1.1 Objects.- 3.1.2 Messages.- 3.1.3 Methods versus functions.- 3.1.4 Classes.- 3.1.5 Inheritance.- 3.1.6 Multiple inheritance.- 3.1.7 Implementation of message-passing.- 3.1.8 Extending classes.- 3.1.9 Self, super and the use of coercions.- 3.1.10 First-class messages: adding overloading.- 3.1.11 Multi-methods.- 3.2 Type checking.- 3.2.1 The types.- 3.2.2 Intuitive typing rules.- 3.3 Object-oriented programming à la CLOS.- 3.3.1 Classes.- 3.3.2 Methods.- 3.3.3 Multiple dispatching.- 3.3.4 Super and coerce.- 3.3.5 Types.- 3.4 Comparison.- 3.5 Conclusion.- 3.6 Bibliographical notes.- 4 The ?&-calculus.- 4.1 Informal presentation.- 4.1.1 Subtyping, run-time types and late binding.- 4.2 The syntax of ?&-calculus.- 4.2.1 Subtyping system.- 4.2.2 Types.- 4.2.3 Terms.- 4.2.4 Type system.- 4.2.5 Reduction Rules.- 4.3 Soundness of the type system.- 4.4 Church-Rosser.- 4.5 Basic encodings.- 4.5.1 Products.- 4.5.2 Simple records.- 4.5.3 Updatable records.- 4.6 ?& and object-oriented programming.- 4.6.1 The “objects as records” analogy.- 4.6.2 Inheritance.- 4.6.3 Binary methods and multiple dispatch.- 4.6.4 Covariance vs. contravariance.- 4.6.5 Class extension.- 4.6.6 First class messages.- 4.6.7 Abstract classes.- 4.7 Related work.- 5 Covariance and contravariance: conflict without a cause.- 5.1 Introduction.- 5.2 The controversy.- 5.3 Covariance in the overloading-based model.- 5.4 Covariance in the record-based model.- 5.5 Practical aspects.- 5.6 Conclusion.- 6 Strong Normalization.- 6.1 The full calculus is not normalizing.- 6.2 Fixed point combinators.- 6.3 The reasons for non normalization.- 6.4 Typed-inductive properties.- 6.5 Strong Normalization is typed-inductive.- 7 Three variations on the theme.- 7.1 Adding explicit coercions.- 7.1.1 Properties.- 7.1.2 More on updatable records.- 7.2 More freedom to the system: ?&+.- 7.3 Unifying overloading and ?-abstraction: ?{}.- 7.3.1 Subject Reduction.- 7.3.2 Church-Rosser.- 7.4 Reference to other work.- 8 Interpretation of object-oriented languages.- 8.1 Formal presentation of KOOL.- 8.1.1 The terms of the language.- 8.1.2 The types of the language.- 8.2 ?_object.- 8.2.1 The type system.- 8.2.2 Some results.- 8.3 Translation.- 8.3.1 Correctness of the type-checking.- 8.3.2 Some remarks.- 8.4 ?_object and ?&.- 8.4.1 The encoding of the types.- 8.4.2 The encoding of the terms.- 9 Imperative features and other widgets.- 9.1 Imperative features.- 9.1.1 Imperative KOOL.- 9.1.2 Imperative ?&-calculus.- 9.1.3 Interpretation.- 9.2 Unique application.- 9.3 Signatures.- 10 Semansttics.- 10.1 Introduction.- 10.2 The completion of overloaded types.- 10.3 Early Binding.- 10.4 Semantics.- 10.4.1 PER as a model.- 10.4.2 Overloaded types as Products.- 10.4.3 The semantics of terms.- 10.5 Summary of the semantics.- III Second order.- 11 Introduction to part III.- 11.1 Loss of information in the record-based model.- 11.1.1 Implicit Polymorphism.- 11.1.2 Explicit Polymorphism.- 11.2 F?.- 11.2.1 Subtyping and typing algorithms.- 11.3 Further features.- 11.3.1 Records and update.- 11.3.2 Quantification over recursive types.- 11.3.3 F-bounded quantification.- 11.3.4 Existential quantification.- 12 Second order overloading.- 12.1 Loss of information in the overloading-based model.- 12.1.1 Type dependency.- 12.2 Type system.- 12.2.1 Some useful results.- 12.2.2 Transitivity elimination.- 12.2.3 Subtyping algorithm and coherence of the system.- 12.3 Terms.- 12.4 Reduction.- 12.4.1 Soundness of the type system.- 12.4.2 Church-Rosser.- 13 Second order overloading and object-oriented programming.- 13.1 Object-oriented programming.- 13.1.1 Extending classes.- 13.1.2 First class messages, super and coerce.- 13.1.3 Typing rules for polymorphic KOOL.- 13.1.4 Multiple dispatch.- 13.1.5 Advanced features.- 13.2 Conclusion.- 14 Conclusion.- 14.1 Object-oriented programming.- 14.2 Proof Theory.- 14.3 Beyond object-oriented programming.- IV Appendixes.- A Specification of KOOL.- A.1 Terms.- A.2 Pretypes.- A.3 Subtyping.- A.4 Auxiliary Notation.- A.5 Typing Rules.- B Formal definition of the translation.- B.1 Without mutually recursive methods.- B.2 With recursive methods.- B.3 Overloaded functions.- B.4 Correctness of the type-checking.