ML with extended pattern matching and subtypes

ABSTRACT

We extend a fragment of the programming language Standard ML by incorporating a more general form of record pattern matching and providing for user-declared subtypes. Together, these two enhancements may be used to support a restricted object-oriented programming style. In keeping with the framework of Standard ML, we present typing rules for the language, and develop an efficient type inference algorithm. We prove that the algorithm is sound with respect to the typing rules, and that it infers a most general typing for every typable expression.

REFERENCES

• BL88: K. Bruce and G. Longo. A modest, model of records, inheritance and bounded quantification. In Third IEEE Syrup. Logic in Computer Science, page (to appear), 1988.
• Car84: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• Coo87: W. Cook. A self-ish model of inheritance. Manuscript, 1987.
• CW85: 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]
• GR83: Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• Mil85: R. Milner. The stemdard ml core language. Polymorphism, 2(2), 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Syrup. on Lisp and Functional Programming.
• Mit84: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• Rey80: 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
• Rob65: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• Sta88: R. Stansifer, Type inference with subtypes, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.88-97, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73568]
• Str86: Bjarne Stroustrup, The C++ programming language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• Wan87: M. Wand. Complete type inference for simple objects. In Proc. 2-nd I~EE Syrup. on Logic in Computer Science, pages 37-44, 1987.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Pattern matching

General Terms:
Algorithms, Languages