ML 2021: Unlocking Multi-Phase Modularity with a Powerful Metalanguage 🔧

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.