Modular Typechecking for Hierarchically Extensible Datatypes and Functions
The International Conference on Functional Programming (ICFP
2002), Pittsburgh PA, Oct. 4-6, 2002.
Colin Bleckner, and
One promising approach for adding object-oriented (OO) facilities to
functional languages like ML is to generalize the
existing datatype and function constructs to be hierarchical and
extensible, so that datatype variants simulate classes and function
cases simulate methods.
This approach allows existing datatypes to be
extended with both new operations and new variants, resolving a
long-standing conflict between the functional and OO styles. However,
previous designs based on this approach have been forced to give up
modular typechecking, requiring whole-program checks to ensure
We describe Extensible ML (EML), an ML-like
language that supports hierarchical, extensible datatypes and functions
while preserving purely modular typechecking. To achieve this result,
EML's type system imposes
a few requirements on datatype and function extensibility, but EML
is still able to express both traditional functional and OO idioms.
We have formalized a core version of EML and proven the
type system sound,
and we have developed a prototype interpreter for the language.