Many module system have been proposed for ML-like languages, differing in particular on how they handle type propagation, i.e., when new abstract types are generated. These designs do not satisfactorily model collaborative systems as they assign each communicating instance its own incompatible abstract type.

We propose a module system that gives a sufficiently precise account of generativity that abstract types defined in separate programs can be equal when desired. We use well-understood theoretical notions such as dependent types and singleton types to model type and more generally module equalities. We keep track of generativity with a very simple effect system. The resulting system is both more tractable and more expressive than most previous accounts. Additionally we provide an operational semantics that preserves types, including abstraction, allowing for the communication-time type checking that we require.

This work is in the line of the Hat and Acute languages developed at INRIA and Cambridge.