Transparent modules with fully syntatic signatures

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.

REFERENCES

• 1: Edoardo Biagioni , Robert Harper , Peter Lee , Brian G. Milnes, Signatures for a network protocol stack: a systems application of Standard ML, Proceedings of the 1994 ACM conference on LISP and functional programming, p.55-64, June 27-29, 1994, Orlando, Florida, United States
• 2: Sandip K. Biswas, Higher-order functors with transparent signatures, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-163, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199478]
• 3: M. B/ume. A compilation manager for SML/NJ. as part of SML/NJ User's Guide, 1995.
• 4: L. Cardelli and X. Leroy. Abstract types and the dot notation. In Proc. Programming Concepts and Methods, pages 479~;04. North Holland, 1990.
• 5: L. Cardelli , D. MacQueen, Persistence and type abstraction, Data types and persistence, Springer-Verlag, London, 1988
• 6: S. Corrieo, B. Ewbank, T. Griffin, J. Meale, and H. Trickey. A tool for developing safe and efficient database transactions. In 15th In. ternational Switching Symposium of the World 7~lecommunications Congress, pages 173-177, April 1995.
• 7: Judicaël Courant, An Applicative Module Calculus, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.622-636, April 14-18, 1997
• 8: Karl Crary , Robert Harper , Sidd Puri, What is a recursive module?, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.50-63, May 01-04, 1999, Atlanta, Georgia, United States
• 9: Matthew Flatt , Matthias Felleisen, Units: cool modules for HOT languages, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.236-248, June 17-19, 1998, Montreal, Quebec, Canada
• 10: L. George. MLRISC: Customizable and reusable code generators. Technical memorandum, Lucent Bell Laboratories, Murray Hill, N$, 1997.
• 11: J.Y. Girard. Interpretation Fonctionnelle et Elimination des Coupures clans l'Arithmetique d'Ordre Superieur. PhD thesis, University of Paris VII, 1972.
• 12: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 13: 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]
• 14: 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]
• 15: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 16: R. Harper and C. Stone. An interpretation of Standard ML in type theory. Technical Report CMU--CS-97-147, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, June 1997.
• 17: Mark P. Jones, Using parameterized signatures to express modular structure, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.68-78, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237731]
• 18: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• 19: 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]
• 20: Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-153, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199476]
• 21: X. Leroy. A syntactic ~eory of type generativity and sharing. Journal of Functional Programming, 6(5): 1-32, September 1996.
• 22: Sheng Liang , Gilad Bracha, Dynamic class loading in the Java virtual machine, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.36-44, October 18-22, 1998, Vancouver, British Columbia, Canada
• 23: M. LiUibr/dge. Translucent Sums: A Foundation far Higher-Order Module Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, May 1997. T~ch Report CMU-CS- 97-122.
• 24: 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]
• 25: 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]
• 26: David B. MacQueen , Mads Tofte, A Semantics for Higher-Order Functors, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.409-423, April 11-13, 1994
• 27: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 28: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 29: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 30: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 31: J.H. Reppy and E. R. Gansner. The eXene library manual. SML/NJ documentations, March 1991.
• 32: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 33: C.V. Russo. Types For Modules. PhD thesis, University of Edinburgh, Edinburgh, UK, June 1998.
• 34: Zhong Shao, Flexible representation analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.85-98, June 09-11, 1997, Amsterdam, The Netherlands
• 35: Zhong Shao, Typed cross-module compilation, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.141-152, September 26-29, 1998, Baltimore, Maryland, United States
• 36: Z. Shoo. Transparent modules with fully syntactic signatures (extended version). Technical Report YALEU/DCS/RR-1181, Dept. of Computer Science, Yale Univ., New Haven, CT, June 1999.
• 37: Bjarne Stroustrup, The C++ Programming Language, Third Edition, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
• 38: 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]
• 39: Andrew Tolmach, Tag-free garbage collection using explicit type parameters, Proceedings of the 1994 ACM conference on LISP and functional programming, p.1-11, June 27-29, 1994, Orlando, Florida, United States

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

General Terms:
Design, Languages, Theory