The FLINT Project








Transparent Modules with Fully Syntactic Signatures (Extended Version)

Last modified: Tue Mar 14 19:29:12 2000 GMT.


Zhong Shao


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.


  • Technical Report YALEU/DCS/TR-1181, Department of Computer Science, Yale University, June 1999.
  • In Proc. 1999 ACM SIGPLAN International Conference on Functional Programming (ICFP'99), Paris, France, pages (to appear), September 1999. ©1999 ACM.

Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page