ML 2021: A metalanguage for multi-phase modularity

Jonathan Sterling presents a type-theoretic metalanguage for multi-phase modularity in ML-style module systems.

Jonathan Sterling and Robert Harper Type abstraction, the phase distinction, and computational effects all play an important role in the design and implementation of ML-style module systems. We propose a simple type theoretic metalanguage φML for multi-phase modularity in which these concepts are treated individually, supporting the definition of high-level modular constructs such as generative and applicative functors, as well as all extant forms of structure sharing.