Correspondence polymorphism for object-oriented languages

ABSTRACT

In this paper we propose a new form of polymorphism for object-oriented languages, called correspondence polymorphism. It lies in a different dimension than either parametric or subtype polymorphism. In correspondence polymorphism, some methods are declared to correspond to other methods, via a correspondence relation. With this relation, it is possible to reuse non-generic code in various type contexts—not necessarily subtyping or matching contexts—without having to plan ahead for this reuse. Correspondence polymorphism has advantages over other expressive object type systems in that programmer-declared types still may be simple, first-order types that are easily understood. We define a simple language LCP that reflects these new ideas, illustrating its behavior with multiple examples. We present formal type rules and an operational semantics for LCP, and establish soundness of the type system with respect to reduction.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165188]
• 3: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.104-118, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99600]
• 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: K. Bruce. Typing in object-oriented languages: achieving expressiveness and safety. Technical report, Williams College, 1996.
• 6: Kim Bruce , Luca Cardelli , Giuseppe Castagna , Gary T. Leavens , Benjamin Pierce, On binary methods, Theory and Practice of Object Systems, v.1 n.3, p.221-242, Fall 1995
• 7: Kim B. Bruce , Angela Schuett , Robert van Gent, PolyTOIL: A Type-Safe Polymorphic Object-Oriented Language, Proceedings of the 9th European Conference on Object-Oriented Programming, p.27-51, August 07-11, 1995
• 8: Kim B. Bruce and Joseph C. Vanderwaart. Semantic-driven language design: type-safe virtual types in object-oriented languages. In Proceedings o} MFPS 99, Electronic Notes in Theoretical Computer Science, to appear.
• 9: Giuseppe Castagna, Covariance and contravariance: conflict without a cause, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.431-447, May 1995 [doi>10.1145/203095.203096]
• 10: Jonathan Eifrig , Scott Smith , Valery Trifonov , Amy Zwarico, An interpretation of typed OOP in a language, Lisp and Symbolic Computation, v.8 n.4, p.357-397, Dec. 1995 [doi>10.1007/BF01018829]
• 11: Jonathan Eifrig , Scott Smith , Valery Trifonov, Sound polymorphic type inference for objects, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.169-184, October 15-19, 1995, Austin, Texas, United States
• 12: Jonathan Eifrig , Scott Smith , Valery Trifonov , Amy Zwarico, Application of OOP type theory: state, decidability, integration, Proceedings of the ninth annual conference on Object-oriented programming systems, language, and applications, p.16-30, October 23-28, 1994, Portland, Oregon, United States
• 13: O. L. Madsen , B. Moller-Pedersen, Virtual classes: a powerful mechanism in object-oriented programming, ACM SIGPLAN Notices, v.24 n.10, p.397-406, Oct. 1989
• 14: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 15: Bertrand Meyer, Object-oriented software construction (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 16: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 17: Ran Rinat , Menachem Magidor, Metaphoric Polymorphism: Taking Code Reuse One Step Further, Proceedings of the 10th European Conference on Object-Oriented Programming, p.449-471, July 08-12, 1996
• 18: Kresten Krab Thorup. Genericity in java with virtual types. In LNCS Vol. 1241: ECOOP '97 conference proceedings. Springer-Verlag, 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Design, Languages, Performance, Theory, Verification