Lalita Jategaonkar
John Mitchell
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.
- 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.Google Scholar
- Car84.L. Cardelli. A semantics of multiple inheritance. In Proc. Int. Syrup. on Semantics of Dat~ Typ~. $ophia-A.~ipolis (F~a.c~), Springer LNCS 173, pages 51-68, June 1984. Google ScholarDigital Library
- Coo87.W. Cook. A self-ish model of inheritance. Manuscript, 1987.Google Scholar
- CW85.L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471-522, 1985. Google ScholarDigital Library
- GR83.A. Goldberg and D. Robson. Smalltalk-80: The language and its implementation. Addison Wesley, 1983. Google ScholarDigital Library
- 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.Google Scholar
- Mit84.J.C. Mitchell. Coercion and type inference (summary). In Proc. 11-th A CM Syrup. on Principles of Programming Languages, pages 175-185, January 1984. Google ScholarDigital Library
- Rey80.J.C. Reynolds. Using Category Theory to Design Implicit Conversions and Generic Operators, pages 211-2580. Springer-Verlag Lecture Notes in Computer Science, Vol. 94, 1980. Google ScholarDigital Library
- Rob65.J.A. Robinson. A machine orient~ed logic based on the resolution principle. JACM, 12(1):23-41, 1965. Google ScholarDigital Library
- Sta88.P~. $ta.nsifer. Type inference with subtypes. In Proc. 15-th A CM Syrup. on Priciples of Programming Languages, pages 88-97, January 1988. Google ScholarDigital Library
- Str86.B. Stroustrop. The C++ Programming Language. Addison-Wesley, 1986. Google ScholarDigital Library
- 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.Google Scholar
Index Terms
- ML with extended pattern matching and subtypes
Recommendations
Type inference with subtypes
POPL '88: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe give an algorithm for type inference in a language with functions, records, and variant records. A similar language was studied by Cardelli who gave a type checking algorithm. This language is interesting because it captures aspects of object-...
Shared subtypes: subtyping recursive parametrized algebraic data types
HASKELL '08A newtype declaration in Haskell introduces a new type renaming an existing type. The two types are viewed by the programmer as semantically different, but share the same runtime representation. When operations on the two semantic views coincide, the ...
Comments