PolyTOIL: A type-safe polymorphic object-oriented language

ABSTRACT

PolyTOIL is a new statically typed polymorphic object-oriented programming language that is provably typesafe. By separating the definitions of subtyping and inheritance, providing a name for the type of self, and carefully defining the type-checking rules, we have obtained a language that is very expressive while supporting modular type-checking of classes. The matching relation on types, which is related to F-bounded quantification, is used both in stating type-checking rules and expressing the bounds on type parameters for polymorphism. The design of PolyTOIL is based on a careful formal definition of type-checking rules and semantics. A proof of type safety is obtained with the aid of a subject reduction theorem.

REFERENCES

• 1: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 2: Martín Abadi , Luca Cardelli, A Theory of Primitive Objects - Scond-Order Systems, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.1-25, April 11-13, 1994
• 3: 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
• 4: Martín Abadi , Luca Cardelli, An Imperative Object Calculus, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.471-485, May 22-26, 1995
• 5: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 6: Arnold, K. and Gosling, J. 1996. Java. Addison-Wesley, Reading MA.
• 7: 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]
• 8: Abadi, M. and Plotkin, G. D. 1990. A PER model of polymorphism and recursive types. In Proceedings of the Symposium on Logic in Computer Science, 355--365.
• 9: Kim B. Bruce , Jon Crabtree , Thomas P. Murtagh , Robert van Gent , Allyn Dimock , Robert Muller, Safe and decidable type checking in an object-oriented language, Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, p.29-46, September 26-October 01, 1993, Washington, D.C., United States
• 10: Kim B. Bruce , Jonathan Crabtree , Gerlad Kanapathy, An Operational Semantics for TOOPLE: A Statically-Typed Object-Oriented Programming Language, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, p.603-626, April 07-10, 1993
• 11: Bruce, K. B., Fiech, A., and Petersen, L. 1997. Subtyping is not a good "match" for object-oriented languages. In Proceedings of ECOOP '97, Lecture Notes in Computer Science, vol. 1241, Springer-Verlag, New York, 104--127.
• 12: Gilad Bracha , David Griswold, Strongtalk: typechecking Smalltalk in a production environment, Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, p.215-230, September 26-October 01, 1993, Washington, D.C., United States
• 13: 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]
• 14: Kim Bruce , John C. Mitchell, PER models of subtyping, recursive types and higher-order polymorphism, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-327, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143230]
• 15: 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]
• 16: Bruce, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Program. 4, 2, 127--206. An earlier version of this paper appeared in the 1993 POPL Proceedings.
• 17: Kim B. Bruce, Foundations of object-oriented languages: types and semantics, MIT Press, Cambridge, MA, 2002
• 18: Bruce, K. B. and van Gent, R. 1993. TOIL: A new type-safe object-oriented imperative language. Tech. Rep. Williams College.
• 19: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• 20: Felice Cardone, Relational Semantics for Recursive Types and Bounded Quantification, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.164-178, July 11-15, 1989
• 21: Peter Canning , William Cook , Walter Hill , Walter Olthoff , John C. Mitchell, F-bounded polymorphism for object-oriented programming, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.273-280, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99392]
• 22: William R. Cook , Walter Hill , Peter S. Canning, Inheritance is not subtyping, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.125-135, December 1989, San Francisco, California, United States [doi>10.1145/96709.96721]
• 23: Cook, W. R. 1989. A proposal for making Eiffel type-safe. In Proceedings of the European Conference on Object-Oriented Programming, 57--72.
• 24: 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]
• 25: Mark Day , Robert Gruber , Barbara Liskov , Andrew C. Myers, Subtypes vs. where clauses: constraining parametric polymorphism, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.156-168, October 15-19, 1995, Austin, Texas, United States
• 26: Margaret A. Ellis , Bjarne Stroustrup, The annotated C++ reference manual, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 27: 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
• 28: Kathleen Fisher , Furio Honsell , John C. Mitchell, A lambda calculus of objects and method specialization, Nordic Journal of Computing, v.1 n.1, p.3-37, Spring 1994
• 29: Kathleen Fisher , John C. Mitchell, On the relationship between classes, objects, and data abstraction, Theory and Practice of Object Systems, v.4 n.1, p.3-25, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<3::AID-TAPO2>3.3.CO;2-2]
• 30: Andreas Gawecki , Florian Matthes, Integrating Subtyping, Matching and Type Quantification: A Practical Perspective, Proceedings of the 10th European Conference on Object-Oriented Programming, p.26-47, July 08-12, 1996
• 31: Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• 32: Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
• 33: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• 34: Dinesh Katiyar , David Luckham , John Mitchell, A type system for prototyping languages, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.138-150, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177838]
• 35: Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 36: Meyer, B. 1995. Static typing and other mysteries of life. Tech. Rep., Interactive Software Engineering, Inc. Text of invited address to OOPSLA '95.
• 37: John C. Mitchell, Toward a typed foundation for method specialization and inheritance, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-124, December 1989, San Francisco, California, United States [doi>10.1145/96709.96719]
• 38: Ole Lehrmann Madsen , Boris Magnusson , Birger Mølier-Pedersen, Strong typing of object-oriented languages revisited, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.140-150, September 1990, Ottawa, Canada
• 39: Pierce, B. C. 1993. Mutable objects. Tech. Rep., University of Edinburgh.
• 40: 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]
• 41: 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]
• 42: 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]
• 43: John C. Reynolds, Using category theory to design implicit conversions and generic operators, Semantics-Directed Compiler Generation, Proceedings of a Workshop, p.211-258, January 14-18, 1980
• 44: Craig Schaffert , Topher Cooper , Bruce Bullis , Mike Kilian , Carrie Wilpolt, An introduction to Trellis/Owl, Conference proceedings on Object-oriented programming systems, languages and applications, p.9-16, September 29-October 02, 1986, Portland, Oregon, United States
• 45: Tesler, L. 1985. Object Pascal report. Tech. Rep. 1, Apple Computer.
• 46: van Gent, R. 1993. TOIL: An imperative type-safe object-oriented language. Williams College Senior Honors Thesis.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Classes and objects

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications
          Subjects: Object-oriented languages
      D.3.3 Language Constructs and Features
          Subjects: Constraints; Polymorphism; Inheritance

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Object-oriented constructs

General Terms:
Languages, Theory

Keywords:
Matching, hash type