Transparent modules with fully syntactic signatures

25Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

Abstract

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 type-theoretic semantics to our calculus and show how to compile it into an Fω-like λ-calculus extended with existential types. © 1999 ACM.

Cite

CITATION STYLE

APA

Shao, Z. (1999). Transparent modules with fully syntactic signatures. SIGPLAN Notices (ACM Special Interest Group on Programming Languages), 34(9), 220–231. https://doi.org/10.1145/317765.317801

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free