Modular typechecking for hierarchically extensible datatypes and functions

ABSTRACT

One promising approach for adding object-oriented (OO) facilities to functional languages like ML is to generalize the existing datatype and function constructs to be hierarchical and extensible, so that datatype variants simulate classes and function cases simulate methods. This approach allows existing datatypes to be easily extended with both new operations and new variants, resolving a long-standing conflict between the functional and OO styles. However, previous designs based on this approach have been forced to give up modular typechecking, requiring whole-program checks to ensure type safety. We describe Extensible ML (eml), an ML-like language that supports hierarchical, extensible datatypes and functions while preserving purely modular typechecking. To achieve this result, eml's type system imposes a few requirements on datatype and function extensibility, but eml is still able to express both traditional functional and OO idioms. We have formalized a core version of eml and proven the associated type system sound, and we have developed a prototype interpreter for the language.

REFERENCES

• 1: Ken Arnold , James Gosling , David Holmes, The Java Programming Language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 2: D. Bonniot. Type-checking multi-methods in ML (a modular approach). In The Ninth International Workshop on Foundations of Object-Oriented Languages, FOOL 9, Portland, Oregon, USA, January 2002.
• 3: François Bourdoncle , Stephan Merz, Type checking higher-order polymorphic multi-methods, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.302-315, January 15-17, 1997, Paris, France [doi>10.1145/263699.263743]
• 4: Gilad Bracha , William Cook, Mixin-based inheritance, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.303-311, September 1990, Ottawa, Canada
• 5: 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]
• 6: Giuseppe Castagna , Giorgio Ghelli , Giuseppe Longo, A calculus for overloaded functions with subtyping, Information and Computation, v.117 n.1, p.115-135, Feb. 15, 1995 [doi>10.1006/inco.1995.1033]
• 7: Craig Chambers, Object-Oriented Multi-Methods in Cecil, Proceedings of the European Conference on Object-Oriented Programming, p.33-56, June 29-July 03, 1992
• 8: Craig Chambers , Gary T. Leavens, Typechecking and modules for multimethods, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.6, p.805-843, Nov. 1995 [doi>10.1145/218570.218571]
• 9: William R. Cook, Object-Oriented Programming Versus Abstract Data Types, Proceedings of the REX School/Workshop on Foundations of Object-Oriented Languages, p.151-178, May 28-June 01, 1990
• 10: Michael Ernst , Craig Kaplan , Craig Chambers, Predicate Dispatching: A Unified Theory of Dispatch, Proceedings of the 12th European Conference on Object-Oriented Programming, p.186-211, July 20-24, 1998
• 11: Robert Bruce Findler , Matthew Flatt, Modular object-oriented programming with units and mixins, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.94-104, September 26-29, 1998, Baltimore, Maryland, United States
• 12: Kathleen Fisher , John Reppy, The design of a class mechanism for Moby, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.37-49, May 01-04, 1999, Atlanta, Georgia, United States
• 13: Kathleen Fisher , John H. Reppy, Extending Moby with Inheritance-Based Subtyping, Proceedings of the 14th European Conference on Object-Oriented Programming, p.83-107, June 12-16, 2000
• 14: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 15: J. Garrigue. Code reuse through polymorphic variants. In Workshop on Foundations of Software Engineering, November 2000.
• 16: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 17: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 18: Stefan Kahrs , Donald Sannella , Andrzej Tarlecki, The definition of extended ML: a gentle introduction, Theoretical Computer Science, v.173 n.2, p.445-484, February 28, 1997 [doi>10.1016/S0304-3975(96)00163-6]
• 19: Shriram Krishnamurthi , Matthias Felleisen , Daniel P. Friedman, Synthesizing Object-Oriented and Functional Design to Promote Re-Use, Proceedings of the 12th European Conference on Object-Oriented Programming, p.91-113, July 20-24, 1998
• 20: Sean McDirmid , Matthew Flatt , Wilson C. Hsieh, Jiazzi: new-age components for old-fasioned Java, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.211-222, October 14-18, 2001, Tampa Bay, FL, USA
• 21: T. Millstein, C. Bleckner, and C. Chambers. Modular typechecking for hierarchically extensible datatypes and functions. Technical Report UW-CSE-02-07-05, Department of Computer Science and Engineering, University of Washington, July 2002. ftp://ftp.cs.washington.edu/tr/2002/07/UW-CSE-02-07-05.pdf.
• 22: Todd D. Millstein , Craig Chambers, Modular Statically Typed Multimethods, Proceedings of the 13th European Conference on Object-Oriented Programming, p.279-303, June 14-18, 1999
• 23: T. Millstein and C. Chambers. Modular statically typed multimethods. Information and Computation, 175(1):76--118, May 2002.
• 24: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 25: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 26: Didier Rémy , Jérôme Vouillon, Objective ML: an effective object-oriented extension to ML, Theory and Practice of Object Systems, v.4 n.1, p.27-50, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4]
• 27: John Reppy , Jon Riecke, Simple objects for Standard ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.171-180, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 28: J. C. Reynolds. User defined types and procedural data structures as complementary approaches to data abstraction. In D. Gries, editor, Programming Methodology, A Collection of Articles by IFIP WG2.3, pages 309--317. Springer-Verlag, New York, NY, 1978.
• 29: Andrew Shalit, The Dylan reference manual: the definitive guide to the new object-oriented dynamic language, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1996
• 30: Matthias Zenger , Martin Odersky, Extensible algebraic datatypes with defaults, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy

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; Syntax
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines; Data types and structures

General Terms:
Design, Languages, Theory

Keywords:
extensible datatypes, extensible functions, modular typechecking