Extending record typing to type parametric modules with sharing

ABSTRACT

We extend term unification techniques used to type extensible records in order to solve the two main typing problems for modules in Standard ML: matching and sharing. We obtain a type system for modules based only on well known unification problems, modulo some equational theories we define. Our formalization is simple and has the elegance of polymorphic type disciplines based on unification. It can be seen as a synthesis of previous work on module and record typing.

REFERENCES

• 1: Maria Virginia Aponte. Typage d'un syst~me de modules paramdtriques avec partage: une application de l'unification dans les thdories dquationnelles. Th&se de doctorat, Universit~ de Paris 7, 1992.
• 2: You-Chin Fuh , Prateek Mishra, Polymorphic Subtype Inference: Closing the Theory-Practice Gap, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.167-183, March 13-17, 1989
• 3: 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
• 4: 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]
• 5: David MacQueen. Modules for standard ML. Polymorphism Newsletter, iI, 1985.
• 6: Robin Milner , Mads Tofte, Commentary on standard ML, MIT Press, Cambridge, MA, 1991
• 7: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 8: Didier R4my. Records and variants as a natural extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989.
• 9: Didier R@my. Algbres Touffues. Application au Typage Polymorphe des Objects Enregistrements dans les Langages Fonctionnels. Th~se de doctorat, Universit de Paris 7, 1990.
• 10: Didier Rmy. Type inference for records in a natural extension of ML. Technical Report 1431, Inria, Rocquencourt, May 1991. Also in {Rem90}, chapter 4.
• 11: Mads Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 1987.
• 12: 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]
• 13: Mitchell Wand. Complete type inference for simple objects. In Second Symposium on Logic In Computer Science, 1987.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Standard ML
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Languages