Abstract
The SML-like module systems are small typed languages of their own. As is, one would expect a proof of their soundness following from a proof of subject reduction. Unfortunately, the subject-reduction property and the preservation of type abstraction seem to be incompatible.
As a consequence, in relevant module systems, the theoretical study of reductions is meaningless, and for instance, the question of normalization of module expressions can not even be considered.
In this paper, we analyze this problem as a misunderstanding of the notion of module definition. We build a variant of the SML module system — inspired from recent works by Leroy, Harper, and Lillibridge — which enjoys the subject reduction property. Type abstraction — achieved through an explicit declaration of the signature of a module at its definition — is preserved. This was the initial motivation. Besides our system enjoys other type-theoretic properties: the calculus is strongly normalizing, there are no syntactic restrictions on module paths, it enjoys a purely applicative semantics, every module has a principal type, and type inference is decidable. Neither Leroy's system nor Harper and Lillibridge's system has all of them.
This research was partially supported by the ESPRIT Basic Research Action Types and by the GDR Programmation cofinanced by MRE-PRC and CNRS.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andrew W. Appel and David B. MacQueen. Separate compilation for Standard ML. In Programming Language Design and Implementation 1994, pages 13–23. ACM Press 1994.
T. Coquand and G. Huet. The Calculus of Constructions. Inf. Comp., 76:95–120 1988.
Judicaël Courant. A module calculus for pure type systems. In Typed Lambda Calculi and Applications 97, LNCS. Springer-Verlag, 1997.
R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st Symposium on Principles of Programming Languages, pages 123–137. ACM Press, 1994.
Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins. Incremental recompilation for Standard ML of New Jersey. Technical Report CMU-CS-94-116, Carnegie-Mellon University, 1994.
R. Harper, R. Milner, and M. Tofte. A type discipline for program modules. In TAP-SOFT 87, volume 250 of LNCS, pages 308–319. Springer-Verlag, 1987.
R. Harper, R. Milner, and M. Tofte. The definition of Standard ML. The MIT Press, 1990.
Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Technical Report CMU-CS-92-191, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1992.
Mark P. Jones. Using parameterized signatures to express modular structures. In 23rd Symposium on Principles of Programming Languages. ACM Press, 1996. To appear.
Xavier Leroy. Manifest types, modules, and separate compilation. In 21st symp. Principles of Progr. Lang., pages 109–122. ACM Press, 1994.
Xavier Leroy. Applicative functors and fully transparent higher-order modules. In 22nd Symposium on Principles of Programming Languages, pages 142–153. ACM Press, 1995.
Xavier Leroy, 1996. Private Communication.
Xavier Leroy. A syntactic theory of type generativity and sharing. To appear in Journal of Functional Programming, 1996.
George C Necula and Peter Lee. Safe kernel extensions without run-time checking. In second symposium on Operating Systems Design and Implementation, 1996.
Don Sannella. Formal program development in Extended ML for the working programmer. In Proc. 3rd BCS/FACS Workshop on Refinement, pages 99–130. Springer Workshops in Computing, 1990.
N. Wirth. Programming in Modula-2. Texts and Monographs in Computer Science. Springer-Verlag, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Courant, J. (1997). An applicative module calculus. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030630
Download citation
DOI: https://doi.org/10.1007/BFb0030630
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive