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.