Xavier Leroy
ABSTRACT
This paper presents a variant of the SML module system that introduces a strict distinction between abstract types and manifest types (types whose definitions are part of the module specification), while retaining most of the expressive power of the SML module system. The resulting module system provides much better support for separate compilation.
- 1.M.-V. Aponte. Extending record typing to type parametric modules with sharing. In 20th symposium Principles of Programming Languages, pages 465-478. ACM Press, 1993. Google Scholar
Digital Library
- 2.L. Birkedal, N. Rothwell, M. Tofte, and D. N. Turner. The ML kit, version 1. Technical report 93/14, DIKU, 1993.Google Scholar
- 3.L. Cardelli. Structural subtyping and the notion of power type. In 15th symposium Pmnciples of Programming Languages, pages 70-79. ACM Press, 1988. Google ScholarDigital Library
- 4.L. Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, pages 431-507. Springer-Verlag, 1989.Google Scholar
- 5.L. Cardelli and X. Leroy. Abstract types and the dot notation. In Proc. IFIP TC2 working conference on programming concepts and methods. North-Holland, 1990.Google Scholar
- 6.L. Cardelli and J. C. Mitchell. Operations on records. In Mathematical Foundations of Programming Semantics, volume 442 of Lecture Notes in Computer Science, pages 22-52, 1989. Google Scholar
- 7.L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing surveys, 17(4):471-522, 1985. Google ScholarDigital Library
- 8.P. Crgut. Separate compilation in SML. Working note, Magic group, ECRC, 1993.Google Scholar
- 9.L. Damas and R. Milner. Principal type-schemes for functional programs, in 9th symposium Principles of Programming Languages, pages 207-212. ACM Press, 1982. Google ScholarDigital Library
- 10.R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21~t symposium Pmnczples of Programming Languages. ACM Press, 1994. Google ScholarDigital Library
- 11.R. Harper, R. Milner, and M. Tofte. A type discipline for program modules. In TAPSOFT 87, volume 250 of Lecture Notes in Computer Sczence, pages 308-319. Springer-Verlag, 1987. Google Scholar
- 12.R. Harper and J. C. Mitchell. On the type structure of Standard ML. A CM Trans. Prog. Lang. Syst., 15(2):211-252, 1993. Google ScholarDigital Library
- 13.R. Harper, J. C. Mitchell, and E. Moggi. Higher-order modules and the phase distinction, in 17th symposium Principles of Programming Languages~ pages 341-354. ACM Press, 1990. Google ScholarDigital Library
- 14.D. MacQueen. Modules for Standard ML. In R. Harper, D. MacQueen, and R. Milner, editors, Standard ML. University of Edinburgh, technical report ECS LFCS 86-2, 1986.Google Scholar
- 15.D. MacQueen. Using dependent types to express modular structure. In 13th symposium Pmnciples of Programming Languages, pages 277-286. ACM Press, 1986. Google ScholarDigital Library
- 16.R. Milner and M. Tofte. Commentary on Standard ML. The MIT Press, 1991. Google ScholarDigital Library
- 17.R. Milner, M. Torte, and R. Harper. The definitwn of Standard ML. The MIT Press, 1990. Google ScholarDigital Library
- 18.J. C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial intelligence and mathematical theory of computahon, pages 305- 330. Academic Press, 1991. Google ScholarDigital Library
- 19.J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. A CM Trans. Prog. Lang. Syst., 10(3):470-502, 1988. Google ScholarDigital Library
- 20.B. C. Pierce. Bounded quantification is undecidable. In 19th symposium Principles of Programming Languages, pages 305-315. ACM Press, 1992. Google ScholarDigital Library
- 21.D. Rdmy. Extending ML type system with a sorted equational theory. Research report 1766, INRIA, 1992.Google Scholar
- 22.J. C. Reynolds. The essence of Algol. In de Bakker and van Vliet, editors, Algomthm~c languages, pages 345- 372. North-Holland, 1981.Google Scholar
- 23.A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. In Lisp and Functional Programming 1992, pages 288-298, 1992. Google ScholarDigital Library
- 24.Z. Shao and A. Appel. Smartest recompilation. In 20th symposium Principles of Programming Languages, pages 439-450. ACM Press, 1993. Google ScholarDigital Library
- 25.M. Tofte. Principal signatures for higher-order program modules. In 19th symposium PmncipIes of Programming Languages, pages 189-199. ACM Press, 1992. Google ScholarDigital Library
- 26.M. Tofte. Type abbreviations in signatures. Message sent to the sml mailing list, Jan. 1992.Google Scholar
- 27.N. Wirth. Programming in Modula-2. Springer-Verlag, 1983. Google ScholarDigital Library
Index Terms
- Manifest types, modules, and separate compilation
Recommendations
Rank 2 intersection types for modules
PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programmingWe propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for ...
Separate compilation for Standard ML
PLDI '94: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementationLanguages that support abstraction and modular structure, such as Standard ML, Modula, Ada, and (more or less) C++, may have deeply nested dependency hierarchies among source files. In ML the problem is particularly severe because ML's powerful ...
Modeling abstract types in modules with open existential types
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe propose F-zip, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as ...
Reviews
Frank Lawrence Friedman
In many languages such as Modula-2 and C++, type specifications are treated as opaque, that is, all exported types are abstract. This feature facilitates separate compilation but is claimed to greatly reduce the expressive power of the language. On the other hand, languages such as SML, which treat type specification as transparent, are claimed to enable the construction of modules that more accurately express program structure, but clearly force compile-time checking of type consistency between the definition and use of a component to be done in a bottom-up order. This paper addresses this problem by presenting a modification to SML in which type specifications are treated as opaque but signatures can be enhanced through the use of manifest type specifications. The combination of these features is shown to adequately support separate compilation while retaining the expressivity provided by SML. It is also shown to subsume a large part of the SML sharing constraint capability. Leroy's paper is far from self-contained, and the abstract does not adequately reflect the paper's main focus. A full understanding of the issues addressed and the claimed improvements made requires a familiarity with SML and its goals as well as an understanding of some basic definitions and ideas expressed in other papers referenced in the bibliography. This style is highly appropriate for the publication containing the paper, but it makes the paper less readily available to a wider audience.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments