ML with Extended Pattern Matching and Subtypes

We extend a representative fragment of the programming language ML by incorporating a more general form of record pattern matching and providing for user-declared subtypes. Together, these two enhancements allow us to write programs in a restricted but relatively natural object-oriented style. In keeping with the framework of 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. In the full paper, additional program examples are presented, and a prototype implementation of the type checker, written in Standard ML, is described.