Transparent Modules with Fully Syntactic Signatures
Last modified: Tue Mar 14 19:29:41 2000 GMT.
Authors
Zhong ShaoAbstract
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 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 and translucent sums 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 type-theoretic semantics to our calculus and show how to compile it into an Fomega-like lambda calculus extended with existential types.
Published
- In Proc. 1999 ACM SIGPLAN International Conference on Functional Programming (ICFP'99), Paris, France, pages (to appear), September 1999. ©1999 ACM.
- Technical Report YALEU/DCS/TR-1181, Department of
Computer Science, Yale University, June 1999.
- Gzipped Postscript [124k]
- BibTeX Entry
