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 longstanding 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: Davide Ancona , Giovanni Lagorio , Elena Zucca, A Formal Framework for Java Separate Compilation, Proceedings of the 16th European Conference on Object-Oriented Programming, p.609-636, June 10-14, 2002
• 2: Davide Ancona , Elena Zucca, True Modules for Java-like Languages, Proceedings of the 15th European Conference on Object-Oriented Programming, p.354-380, June 18-22, 2001
• 3: Davide Ancona , Elena Zucca, A calculus of module systems, Journal of Functional Programming, v.12 n.2, p.91-132, March 2002 [doi>10.1017/S0956796801004257]
• 4: Ken Arnold , James Gosling , David Holmes, The Java Programming Language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 5: Bonniot, D. 2002. 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).
• 6: 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]
• 7: 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
• 8: 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]
• 9: Luca Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.266-277, January 15-17, 1997, Paris, France [doi>10.1145/263699.263735]
• 10: 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]
• 11: Craig Chambers , Weimin Chen, Efficient multiple and predicated dispatching, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.238-255, November 01-05, 1999, Denver, Colorado, United States
• 12: 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]
• 13: Curtis Clifton , Gary T. Leavens , Craig Chambers , Todd Millstein, MultiJava: modular open classes and symmetric multiple dispatch for Java, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.130-145, October 2000, Minneapolis, Minnesota, United States
• 14: 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
• 15: Sophia Drossopoulou , Susan Eisenbach , David Wragg, A Fragment Calculus Towards a Model of Separate Compilation, Linking and Binary Compatibility, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.147, July 02-05, 1999
• 16: Dominic Duggan , Constantinos Sourelis, Mixin modules, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.262-273, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 17: Dominic Duggan , Ching-Ching Techaubol, Modular mixin-based inheritance for application frameworks, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.223-240, October 14-18, 2001, Tampa Bay, FL, USA
• 18: 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
• 19: 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
• 20: 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
• 21: 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
• 22: Matthew Flatt , Matthias Felleisen, Units: cool modules for HOT languages, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.236-248, June 17-19, 1998, Montreal, Quebec, Canada
• 23: 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]
• 24: You-Chin Fuh , Prateek Mishra, Type inference with subtypes, Theoretical Computer Science, v.73 n.2, p.155-175, June 22, 1990
• 25: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 26: Garrigue, J. 2000. Code reuse through polymorphic variants. In Workshop on Foundations of Software Engineering, November.
• 27: 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
• 28: Tom Hirschowitz , Xavier Leroy, Mixin Modules in a Call-by-Value Setting, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.6-20, April 08-12, 2002
• 29: My Hoang , John C. Mitchell, Lower bounds on type inference with subtypes, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.176-185, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199481]
• 30: 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]
• 31: 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]
• 32: 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
• 33: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• 34: 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
• 35: Todd David Millstein , Craig Chambers, Reconciling software extensibility with modular program reasoning, 2003
• 36: Todd Millstein , Colin Bleckner , Craig Chambers, Modular typechecking for hierarchically extensible datatypes and functions, ACM SIGPLAN Notices, v.37 n.9, p.110-122, September 2002
• 37: 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
• 38: Millstein, T. and Chambers, C. 2002. Modular statically typed multimethods. Information and Computation 175, 1, 76--118 (May).
• 39: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 40: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 41: Johan Nordlander, Pragmatic subtyping in polymorphic languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.216-227, September 26-29, 1998, Baltimore, Maryland, United States
• 42: 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]
• 43: Benjamin C. Pierce , David N. Turner, Local type inference, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.1-44, Jan. 2000 [doi>10.1145/345099.345100]
• 44: 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]
• 45: 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
• 46: Reynolds, J. C. 1978. 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, 309--317. Springer-Verlag, New York, NY.
• 47: 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
• 48: Wadler, P. 1990. Linear types can change the world! In M. Broy and C. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 7--359. North Holland (Apr.).
• 49: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 50: 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.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures; Procedures, functions, and subroutines; Classes and objects

General Terms:
Design, Languages, Theory

Keywords:
Extensible datatypes, extensible functions, modular typechecking