Transparent modules with fully syntactic signatures

ML-style modules are valuable in the development and mainte-nance of large software systems, unfortunately, none of the existing languages support them in a fully satisfactory manner. The offi-cial SML’97 Definition does not allow higher-order functors, so a module that refers to externally defined functors cannot accurately describe its import interface. MacQueen and Tofte [26] extended SML’97 with fully transparent higher-order functors, but their sys-tem does not have a type-theoretic semantics thus fails to support fully syntactic signatures. The systems of manifest types [19, 20] and translucent sums [12] support fully syntactic signatures but they may propagate fewer type equalities than fully transparent functors. This paper presents a module calculus that supports both fully transparent higher-order functors and fully syntactic signa-tures (and thus true separate compilation). We give a simple type-theoretic semantics to our calculus and show how to compile it into an-like -calculus extended with existential types.