Higher-order functors with transparent signatures

ABSTRACT

The programming language Standard ML provides first-order functors, i.e. modules parameterized by modules. First-order functors in the language have a simple and elegant static semantics. The type structure of higher-order modules, i.e. modules parameterized by functors, is well understood. But it is only in the recent past that we have seen an implementation of higher-order functors with a formally defined static semantics in a dialect of Standard ML, SML/NJ. A study of this static semantics shows it to be much more complicated than the static semantics of first-order functors. This paper investigates whether we can trade some semantic features in the module language to obtain a simpler static semantics, closer in spirit to that of first-order functors. This work helps in a conceptual understanding of the semantics of higher-order modules.

REFERENCES

• 1: L. Cardelli and X. Leroy. Abstract types and the dot notation. Research Report 56, DEC Systems, Palo Alto, March 1990.
• 2: 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]
• 3: 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]
• 4: G. Huet. A unification algorithm for typed A-calculus. Theoretical Computer Science, 1:27-57, 1975.
• 5: 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]
• 6: 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]
• 7: 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
• 8: D. Miller. A logic programming language. Journal of Logic and Computation, 1:497-536, 1991.
• 9: Robin Milner , Mads Tofte, Commentary on standard ML, MIT Press, Cambridge, MA, 1991
• 10: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 11: 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]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Standard ML

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics

General Terms:
Algorithms, Languages, Theory, Verification