Positive subtyping

ABSTRACT

The statement S≤T in a &lgr;-calculus with subtyping is traditionally interpreted by a semantic coercion function of type [[S]]→[[T]] that extracts the “T part” of an element of S. If the subtyping relation is restricted to covariant positions, this interpretation may be enriched to include both the implicit coercion and an overwriting function put[S,T] ∈ [[S]]→[[T]]→[[S]] that updates the T part of an element of S. We give a realizability model and a sound equational theory for a second-order calculus of positive subtyping.Though weaker than familiar calculi of bounded quantification, positive subtyping retains sufficient power to model objects, encapsulation, and message passing. Moreover, inheritance may be implemented very straightforwardly in this setting, using the put functions arising from ordinary subtyping of records in place of the sophisticated systems of record extension and update often used for this purpose. The equational laws relating the behavior of coercions and put functions can be used to prove simple properties of the resulting classes in such a way that proofs for superclasses are “inherited” by subclasses.

REFERENCES

• 1: Martín Abadi , Luca Cardelli, A Theory of Primitive Objects - Untyped and First-Order Systems, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.296-320, April 19-22, 1994
• 2: Roberto M. Amadio, Recursion over realizability structures, Information and Computation, v.91 n.1, p.55-85, March 1991 [doi>10.1016/0890-5401(91)90074-C]
• 3: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 4: Kim B. Bruce, Safe type checking in a statically-typed object-oriented programming language, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.285-298, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158650]
• 5: Kim B. Bruce , Giuseppe Longo, A modest model of records, inheritance, and unbounded quantification, Information and Computation, v.87 n.1-2, p.196-240, July/August 1990 [doi>10.1016/0890-5401(90)90062-M]
• 6: Luca Cardelli. Notes about F.#.. Unpublished manuscript, October 1990.
• 7: Luca Cardelli, Extensible records in a pure calculus of subtyping, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 8: Luca Cardelli , Giuseppe Longo, A semantic basis for quest, Proceedings of the 1990 ACM conference on LISP and functional programming, p.30-43, June 27-29, 1990, Nice, France [doi>10.1145/91556.91586]
• 9: Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An extension of system F with subtyping, Information and Computation, v.109 n.1-2, p.4-56, Feb. 15/March 1994 [doi>10.1006/inco.1994.1013]
• 10: Luca Cardelli , John C. Mitchell, Operations on records, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 11: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 12: Adriana B. Compagnoni, Decidability of Higher-Order Subtyping with Intersection Types, Selected Papers from the 8th International Workshop on Computer Science Logic, p.46-60, September 25-30, 1994
• 13: Adriana B. Compagnoni and Benjamin C. Pierce. Multiple inheritance via intersection types. Technical Report ECS-LFCS-93-275, LFCS, University of Edinburgh, August 1993. Also available as Catholic University Nijmegen computer science technicM report 93- 18.
• 14: William R. Cook, A denotational semantics of inheritance, 1989
• 15: Pierre-Louis Curien , Giorgio Ghelli, Coherence of subsumption, minimum typing and type-checking in F≤, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 16: Kathleen Fisher , John C. Mitchell, Notes on Typed Object-Oriented Programming, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.844-885, April 19-22, 1994
• 17: Martin Hofmann and Benjamin Pierce. Positive subtyping. Technical Report ECS-LFCS-94-303, LFCS, University of Edinburgh, September 1994.
• 18: Martin Hofmann , Benjamin C. Pierce, A Unifying Type-Theoretic Framework for Objects, Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science, p.251-262, February 24-26, 1994
• 19: Samuel N. Kamin , Uday S. Reddy, Two semantic models of object-oriented languages, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 20: Gary T. Leavens. Inheritance of interface specifications (extended abstract). Technical Report TR#93-23, Department of Computer Science, Iowa State University, September 1993.
• 21: Wolfgang Naraschewski. Verifikation objektorientierter Programme mit LEGO. Studienarbeit, Universit#it Erlangen, 1994. To appear.
• 22: F J Oles, Type algebras, functor categories and block structure, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 23: Benjamin C. Pierce, Bounded quantification is undecidable, Information and Computation, v.112 n.1, p.131-165, July 1994 [doi>10.1006/inco.1994.1055]
• 24: Benjamin C. Pierce , David N. Turner, Object-oriented programming without recursive types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.299-312, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158653]
• 25: Martin Steffen , Benjamin C. Pierce, Higher-Order Subtyping, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi, p.511-530, June 06-10, 1994

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Theory