Mixin' up the ML module system
Venue
Transactions on Programming Languages and Systems, vol. 35 (1) (2013)
Publication Year
2013
Authors
Andreas Rossberg, Derek Dreyer
BibTeX
Abstract
ML modules provide hierarchical namespace management, as well as fine-grained
control over the propagation of type information, but they do not allow modules to
be broken up into mutually recursive, separately compilable components. Mixin
modules facilitate recursive linking of separately compiled components, but they
are not hierarchically composable and typically do not support type abstraction. We
synthesize the complementary advantages of these two mechanisms in a novel module
system design we call MixML. A MixML module is like an ML structure in which some
of the components are specified but not defined. In other words, it unifies the ML
structure and signature languages into one. MixML seamlessly integrates
hierarchical composition, translucent ML-style data abstraction, and mixin-style
recursive linking. Moreover, the design of MixML is clean and minimalist; it
emphasizes how all the salient, semantically interesting features of the ML module
system (and several proposed extensions to it) can be understood simply as stylized
uses of a small set of orthogonal underlying constructs, with mixin composition
playing a central role. We provide a declarative type system for MixML, including
two important extensions: higher-order modules, and modules as first-class values.
We also present a sound and complete, three-pass type checking algorithm for this
system. The operational semantics of MixML is defined by an elaboration translation
into an internal core language called LTG – namely, a polymorphic lambda calculus
with single-assignment references and recursive type generativity – which employs a
linear type and kind system to track definedness of term and type imports.
