Transparent Modules with Fully Syntactic Signatures

ML-style modules are valuable in the development and maintenance of large software systems, unfortunately, none of the existing languages support them in a fiilly satisfactory manner. The official 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 system 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 signatures (and thus true separate compilation). We give a simple typetheoretic semantics to our calculus and show how to compile it into an F(w)-like A-calculus extended with existential types.