Type-safe generation of modules in applicative and generative styles

Abstract

The MetaML approach for multi-stage programming provides the static guarantee of type safety and scope safety for generated code, regardless of the values of static parameters. Modules are indispensable to build large-scale programs in ML-like languages, however, they have a performance problem. To solve this problem, several languages proposed recently allow one to generate ML-style modules. Unfortunately, those languages had the problems of limited expressiveness, incomplete proofs, and code explosion.

This paper proposes two-stage programming languages for module generation, which solve all the above issues. Our languages accommodate two styles: first-class modules with generative functors and second-class modules with applicative functors. Module generation in both styles is shown to have their own merits by concrete examples. We present type systems, and type-preserving translations from our languages to plain MetaOCaml. We also show the results of performance measurements, which confirms the effectiveness of our languages.