AbstractStandard ML is a statically typed programming language that is suited for the construction of both small and large programs. ``Programming in the small'' is captured by Standard ML's Core language. ``Programming in the large'' is captured by Standard ML's Modules language that provides constructs for organising related Core language definitions into self-contained modules with descriptive interfaces. While the Core is used to express details of algorithms and data structures, Modules is used to express the overall architecture of a software system. The Modules and Core languages are stratified in the sense that modules may not be manipulated as ordinary values of the Core. This is a limitation, since it means that the architecture of a program cannot be reconfigured according to run-time demands. We propose a novel and practical extension of the language that allows modules to be manipulated as first-class values of the Core language.
Categories and Subject Descriptors: D.3 [Programming Languages]
Additional Key Words and Phrases: existential types, first-class modules, Standard ML, type theory
Selected references
- Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Conference Record of POPL '94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 123-137, Portland, Oregon, January 1994.
- Robert Harper and John C. Mitchell. On the type structure of standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211-252, April 1993.
- Dinesh Katiyar, David Luckham, and John C. Mitchell. A type system for prototyping languages. In Conference Record of POPL '94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 138-150, Portland, Oregon, January 1994.
- Xavier Leroy. Manifest types, modules, and separate compilation. In Conference Record of POPL '94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 109-122, Portland, Oregon, January 1994.
- Xavier Leroy. Applicative functors and fully transparent higher-order modules. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 142-153, San Francisco, California, January 1995.
- David MacQueen. Using dependent types to express modular structure. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 277-286, St. Petersburg Beach, Florida, January 1986.
- David B. MacQueen and Mads Tofte. A semantics for higher-order functors. In Donald Sannella, editor, Programming Languages and Systems -- ESOP'94, 5th European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 409-423, Edinburgh, U.K., 11-13 April 1994. Springer.
- Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348-375, December 1978.
- John C. Mitchell, Sigurd Meldal, and Neel Madhav. An extension of Standard ML modules with subtyping and inheritance. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 270-278, Orlando, Florida, January 1991.
- John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470-502, July 1988.
- Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Conference Record of POPL '96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 54-67, St. Petersburg Beach, Florida, 21-24 January 1996.