Higher-order modules and the phase distinction

ABSTRACT

In earlier work, we used a typed function calculus, XML, with dependent types to analyze several aspects of the Standard ML type system. In this paper, we introduce a refinement of XML with a clear compile-time/run-time phase distinction, and a direct compile-time type checking algorithm. The calculus uses a finer separation of types into universes than XML and enforces the phase distinction using a nonstandard equational theory for module and signature expressions. While unusual from a type-theoretic point of view, the nonstandard equational theory arises naturally from the well-known Grothendieck construction on an indexed category.

REFERENCES

• BL84: 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
• BMM89: Kim B. Bruce , Albert R. Meyer , John C. Mitchell, The semantics of second-order lambda calculus, Information and Computation, v.85 n.1, p.76-134, March 1990 [doi>10.1016/0890-5401(90)90044-I]
• C+86: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• Car88: L. Cardelli. Phase distinctions in type theory. Manuse'ript, 1988.
• Gir71: J.-Y.. Girard. Une extension de l'interpretation de G6del ~ l'analyse, et son application k l'61imination des coupures'dans l'analyse et la th6orie des types. In j.E. Fenstad, editor, 2nd Scandinavian Logic Symposium, pages 63-92. North-Holland, 1971.
• Gir72: J.-Y. Girard. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. These D'Etat, Universite Paris VII, 1972.
• HMM86: R. Harper, D.B. MacQueen, and R. Milner. Standard ml. Technical Report ECS-LFCS-86-2, Lab. for Foundations of Computer Science, University of Edinburgh, March 1986.
• HMT87a: R. Harper, R. Milner, and M. Tofte. Tile semantics of standard ML. Technical Report ECS-LFCS-87-36, Lab. for Foundations of Computer Science, University of Edinburgh, August 1987.
• HMT87b: 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
• Mac86: 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]
• Mar84: P. Martin-L6f. lntuitionistic Type Theory. Bibliopolis, Napoli, 1984.
• MH88: 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]
• Mog89a: Eugenio Moggi, A Category-theoretic Account of Program Modules, Category Theory and Computer Science, p.101-117, September 05-08, 1989
• Mog89b: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• MP88: 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]
• NPS88: B. Nordstrom, K. Peterson, and J. Smith. Programming in martin-16f's type theory. University of Gothenburg { Chalmers {nstitue of Technology, Book draft of Midsummer 1988.
• Rey74: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• Tof87: M. Torte. Operational Semanlics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 198-/.

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: ML

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Denotational semantics

General Terms:
Algorithms, Languages