Type-Checking Higher-Order Polymorphic Multimethods
We present a new predicative and decidable type system, called ML-sub, suitable
for languages that integrate functional programming and parametric
polymorphism in the tradition of ML, and class-based object-oriented
programming and higher-order multi-methods in the tradition of CLOS. 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-sub 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 à la XML
with multi-methods, show that the resulting system has decidable minimal
types, and discuss subject reduction. Finally, we propose a new
object-oriented programming language based on the ML-sub type system.
[PostScript, PDF, © 1997 ACM]
[ML-sub Technical Report]
[An implementation of
ML-sub] [The Jazz rogramming language]
François Bourdoncle