Type Inference with Extended Pattern Matching and Subtypes

Article type: Research Article

Authors: Jategaonkar, Lalita A.^a | Mitchell, John C.^b

Affiliations: [a] Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, USA, E-mail: lalita@theory.lcs.mit.edu | [b] Department of Computer Science, Stanford University, Stanford, CA, USA, E-mail: mitchell@cs.stanford.edu

Abstract: We study a type system, in the spirit of ML and related languages, with two novel features: a general form of record pattern matching and a provision for user-declared subtypes. Extended pattern matching allows a function on records to be applied to any record that contains a minimum set of fields and permits the additional fields of the record to be manipulated within the body of the function. Together, these two enhancements may be used to support a restricted object-oriented programming style. We define the type system using inference rules, and develop a 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.

DOI: 10.3233/FI-1993-191-206

Journal: Fundamenta Informaticae, vol. 19, no. 1-2, pp. 127-165, 1993