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 fully 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 ¡£¢...

• Type: Conference
• Year: 1999
• Where: ICFP
• Authors: Zhong Shao
• Keywords: ICFP 1999, Official Sml’97 Definition, Programming Languages, Syntactic Signatures, Transparent Functors