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 gen- erative and non-generative types. Unlike other systems, the gener- ativity of a type is reflected directly in the signature of the mod- ule 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 genera- tive 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 ab- straction. Categories and Subject Descriptors D.3.3 [Language Constructs and Features]: Modules General Terms Modules, Type Systems, Abstraction Keywords ML Modules, Generativity, Standard ML, Objective