Applicative functors and fully transparent higher-order modules

ABSTRACT

we present a variety of the Standard ML module system where parameterized abstract types (i.e. functors returning generative types) map provably equal arguments to compatible abstract types, instead of generating distinct types at each applications as in Standard ML. This extension solves the full transparency problem (how to give syntactic signatures for higher-order functors that express exactly their propagation of type equations), and also provides better support for non-closed code fragments.

REFERENCES

• 1: Andrew W. Appel , David B. MacQueen, Separate compilation for Standard ML, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.13-23, June 20-24, 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: L. Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal description of programming concepts, pages 431-507. Springer-Verlag, 1989.
• 4: L. Cardelli and X. Leroy. Abstract types and the dot notation. In M. Broy and C. B. Jones, editors, Proceedings IFIP TC2 working conference on programming concepts and methods, pages 479-504. North-Holland, 1990.
• 5: L. Cardelli , D. MacQueen, Persistence and type abstraction, Data types and persistence, Springer-Verlag, London, 1988
• 6: P. Cr#gut. Compilation s#par#e pour un langage de modules avec types g#n#ratifs, Sept. 1994. Presentation given at the 1994 meeting of the G.D.R. "Programmation", C.N.R.S.
• 7: 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]
• 8: R. Harper , R. Milner , M. Tofte, A type discipline for Program modules, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.308-319, March 1987, Pisa, Italy
• 9: 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]
• 10: 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]
• 11: X. Leroy. A syntactic approach to type generativity and sharing (extended abstract). In Proc. 199# Workshop on ML and its applications, pages 1-12. Research report 2265, INRIA, 1994.
• 12: 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]
• 13: 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
• 14: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 15: John C. Mitchell, On the equivalence of data representations, Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, Academic Press Professional, Inc., San Diego, CA, 1991
• 16: 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]
• 17: J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing '83, pages 513-523. North-Holland, 1983.
• 18: F. Rouaix. The ALCOOL 90 report. INRIA, 1992. Included in the distribution available on ftp. im=ia, f2=.

INDEX TERMS

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

          Nouns: Standard ML

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages