Type Generativity in Higher-Order Module Systems

Abstract

We present a higher-order module system similar to those found in Standard ML and Objective Caml. Our system allows both generative and non-generative types. Unlike other systems, the generativity of a type is reflected directly in the signature of the module in which it is declared, allowing a more direct analysis of type abstraction and generativity. Our module system can express both generative and applicative functors, and allows mixing of generative and non-generative types within a single module. This gives the programmer greater control over type generativity, and brings a new perspective to the relationship between the two styles of abstraction.