Type Checking Higher-Order Polymorphic Multi-Methods

We present a new predicative and decidable type system, called ML , suitable for languages that integrate functional programming and parametric polymorphism in the tradition of ML [21, 28], and class-based objectoriented programming and higher-order multi-methods in the tradition of CLOS [12]. Instead of using extensible records as a foundation for object-oriented extensions of functional languages, we propose to reinterpret ML datatype declarations as abstract and concrete class declarations, and to replace pattern matching on run-time values by dynamic dispatch on run-time types. ML is based on universally quantified polymorphic constrained types. Constraints are conjunctions of inequalities between monotypes built from type constructors organized into extensible and partially ordered classes. We give type checking rules for a small, explicitly typed functional language `a la XML [20] with multi-methods, show that the resulting system has decidable minimal types, and discuss subject ..