A type-theoretic approach to higher-order modules with sharing

ABSTRACT

The design of a module system for constructing and maintaining large programs is a difficult task that raises a number of theoretical and practical issues. A fundamental issue is the management of the flow of information between program units at compile time via the notion of an interface. Experience has shown that fully opaque interfaces are awkward to use in practice since too much information is hidden, and that fully transparent interfaces lead to excessive interdependencies, creating problems for maintenance and separate compilation. The “sharing” specifications of Standard ML address this issue by allowing the programmer to specify equational relationships between types in separated modules, but are not expressive enough to allow the programmer complete control over the propagation of type information between modules. These problems are addressed from a type-theoretic viewpoint by considering a calculus based on Girard's system F&ohgr;. The calculus differs form those considered in previous studies by relying exclusively on a new form of weak sum type to propagate information at compile-time, in contrast to approaches based on strong sums which rely on substitution. The new form of sum type allows for the specification of equational, as well as type and kind, information in interfaces. This provides complete control over the propagation of compile-time information between program units and is sufficient to encode in a straightforward way most users of type sharing specifications in Standard ML. Modules are treated as “first-class” citizens, and therefore the system supports higher-order modules and some object-oriented programming idioms; the language may be easily restricted to “second-class” modules found in ML-like languages.

REFERENCES

• 1: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 2: Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In J. Maluszynski and M. Wirsing, editors, Third lnt'l Syrup. on Prog. Lang. implementation and Logic Programming, pages 1-13, New York, August 1991. Springer-Verlag.
• 3: Edoardo Biagioni , Robert Harper , Peter Lee, Standard ML Signatures for a Protocol Stack, Carnegie Mellon University, Pittsburgh, PA, 1993
• 4: Hans Boehm , Alan J. Demers , James E. Donahue, An Informal Description of Russell, Cornell University, Ithaca, NY, 1980
• 5: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• 6: Luca Cardelli, A semantics of multiple inheritance., Proc. of the international symposium on Semantics of data types, p.51-67, July 1984, Sophia-Antipolis, France
• 7: Luca Cardelli. Typeful programming. Technical Report 45, DEC SRC, 1989.
• 8: Luca Cardelli, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. Modula-3 report (revised). Technical Report 52, DEC Systems Research Center, Palo Alto, CA, November 1989.
• 9: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• 10: Luca Cardelli and Leroy Xavier. Abstract types and the dot notation. Technical Report 56, DEC SRC, Palo Alto, CA, March 1990.
• 11: Eric Cooper, Robert Harper, and Peter Lee. The Fox project: Advanced development of systems software. Technical Report CMU-CS-91-178, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, August 1991.
• 12: Nicolas G. de Bruijn. A survey of the project AU- TOMATH. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 589-606. Academic Press, 1980.
• 13: Emden Gansner and John Reppy. eXene. In Robert Harper, editor, Third international Workshop on Standard ML, Pittsburgh, PA, September 1991. School of Computer Science, Carnegie Mellon University.
• 14: Jean-Yves Girard. interprgtation Fonctionnelle et Elimination des Coupures dans l'Arithmgtique d'Ordre Supdrieure. PhD thesis, Universitfi Paris VII, 1972.
• 15: Robert Harper. Introduction to Standard ML. Technical Report ECS-LFCS-86-14, Laboratory for the Foundations of Computer Science, Edinburgh University, September 1986.
• 16: Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158630]
• 17: Robert Harper, David MacQueen, and Robin Milner. Standard ML. Technical Report ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science, Edinburgh University, March 1986.
• 18: Robert Harper, David MacQueen, and Robin Milner. Standard ML. Technical Report ECS-LFCS-86-2, Laboratory for the Foundations of Computer Science, Edinburgh University, March 1986.
• 19: Robert Harper , John C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.211-252, April 1993 [doi>10.1145/169701.169696]
• 20: Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
• 21: James G. Hook, Understanding Russell–a first attempt, Proc. of the international symposium on Semantics of data types, p.69-85, July 1984, Sophia-Antipolis, France
• 22: Proc. of the international symposium on Semantics of data types, July 1984
• 23: Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
• 24: Barbara Liskov, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
• 25: Zhaolui Luo, Robert Pollack, and Paul Taylor. How to use Lego: A preliminary user's manual. Technical Report LFCS-TN-27, Laboratory for the Foundations of Computer Science, Edinburgh University, October 1989.
• 26: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• 27: David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
• 28: David MacQueen, An implementation of standard ML modules, Proceedings of the 1988 ACM conference on LISP and functional programming, p.212-223, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62704]
• 29: Per Martin-LSf. Constructive mathematics and computer programming, in Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-175. North-Holland, 1982.
• 30: David C. J. Matthews. POLY report. Technical Report 28, Computer Laboratory, University of Cambridge, 1982.
• 31: Robin Milner , Mads Tofte, Commentary on standard ML, MIT Press, Cambridge, MA, 1991
• 32: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 33: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• 34: John Mitchell , Sigurd Meldal , Neel Madhav, An extension of standard ML modules with subtyping and inheritance, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-278, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99620]
• 35: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• 36: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 37: Benjamin C. Pierce, Bounded quantification is undecidable, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.305-315, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143228]
• 38: Benjamin Crawford Pierce, Programming with intersection types and bounded polymorphism, Carnegie Mellon University, Pittsburgh, PA, 1992
• 39: Chris Reade, Elements of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1989
• 40: Nick Rothwell. Functional compilation from the Standard ML core language to lambda calculus. Technical Report ECS-LFCS-92-235, Laboratory for the Foundations of Computer Science, Edinburgh University, Edinburgh, Scotland, September 1992.
• 41: Nick Rothwell. Miscellaneous design issues in the ML kit. Technical Report ECS-LFCS-92-237, Laborator) for the Foundations of Computer Science, Edinburg~ University, Edinburgh, Scotland, September 1992.
• 42: Zhong Shao , Andrew W. Appel, Smartest recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.439-450, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158702]
• 43: Mads Tofte, Principal signatures for higher-order program modules, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.189-199, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143206]
• 44: Mads ToRe. Type abbreviations in signatures. Unpublished manuscript, August 1993.
• 45: Diedrik T. van Daalen. The Language Theory of A U- TOMATH. PhD thesis, Technical University of Eindhoven, Eindhoven, Netherlands, 1980.
• 46: Niklaus Wirth, Programming in MODULA-2 (3rd corrected ed.), Springer-Verlag New York, Inc., New York, NY, 1985

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory, Verification