Technical Report: A Syntactic Approach to Structure Generativity -- A Referentially-Transparent Higher-Order Module Language

Advanced module systems like Standard ML's support structure generativity. Structure generativity denotes the mechanism that parameterized modules (functors) generate a "new" module instance (structure) for every application to a suitable argument. This operational behaviour is essentially a side effect. Since interfaces in general depend on module instances, module instances are computationally characterised as "stamps" for the purpose of interface-checking. This paper presents a typed module calculus that makes instances of modules syntactically apparent in expressions and interfaces. The module calculus has a simple rewriting semantics without side effects. Interface-checking is based on a type system with dependent functions, strong sums and additionally a non-standard variant of weak sums. A module system derived from the module calculus forms a separate layer above some typed core language. As a demonstrating example, we sketch M/SML, a module language on top of core SML.