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 quanti ed polymorphic constrained types. Constraints are conjunctions of inequalities between monotypes built from type constructors organizedinto 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 reduc...

• Type: Conference
• Year: 1997
• Where: POPL
• Authors: François Bourdoncle, Stephan Merz
• Keywords: Decidable Type System, ML Datatype Declarations, POPL 1997, Programming Languages, Type System