What is a recursive module?

ABSTRACT

A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can impede modular programming by forcing mutually-dependent components to be consolidated into a single module. Recently there have been several proposals for module systems that admit cyclic dependencies, but it is not clear how these proposals relate to one another, nor how one might integrate them into an expressive module system such as that of ML.To address this question we provide a type-theoretic analysis of the notion of a recursive module in the context of a "phase-distinction" formalism for higher-order module systems. We extend this calculus with a recursive module mechanism and a new form of signature, called a recursively dependent signature, to support the definition of recursive modules. These extensions are justified by an interpretation in terms of more primitive language constructs. This interpretation may also serve as a guide for implementation.

REFERENCES

• 1: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 2: Davide Ancona , Elena Zucca, An algebra of mixin modules, Selected papers from the 12th International Workshop on Recent Trends in Algebraic Development Techniques, p.92-106, July 01, 1997
• 3: Matthias Blume, Hierarchical modulatory and intermodule optimization, Princeton University, Princeton, NJ, 1998
• 4: Luca Cardelli. Phase distinctions in type theory. Unpublished manuscript.
• 5: Karl Crary, Robert Harper, Perry Cheng, Leaf Petersen, and Chris Stone. Transparent and opaque interpretations of datatypes. Technical Report CMU-CS-98-177, Carnegie Mellon University, School of Computer Science, November 1998.
• 6: Dominic Duggan , Constantinos Sourelis, Mixin modules, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.262-273, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 7: Dominic Duggan and Constantinos Sourelis. Parameterized modules, recursive modules, and mixin modules, in 1998 A CM SIGPLAN Workshop on ML, pages 87-96, Baltimore, Maryland, September 1998.
• 8: 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
• 9: 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]
• 10: 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]
• 11: 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]
• 12: Robert Harper , Christopher Stone, A type-theoretic interpretation of standard ML, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 13: 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]
• 14: Xavier Leroy. The Objective Carol system: Documentation and user's guide. Available at http://pauillac, inria, fr/ocaml/htmlman/., 1996.
• 15: 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]
• 16: Robin Milner , Mads Tofte , Robert Harper, The Definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 17: Géraud Sénizergues, The Equivalence Problem for Deterministic Pushdown Automata is Decidable, Proceedings of the 24th International Colloquium on Automata, Languages and Programming, p.671-681, July 07-11, 1997
• 18: Zhong Shao. An overview of the FLINT/ML compiler. In Proceedings of the 1997 A CM SIGPLAN Workshop on Types in Compilation, Kyoto, Japan, June 1997.
• 19: Zhong Shao. Equality of recursive types. (Private communication), September 1998.
• 20: 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
• 21: Emin Giin Sirer, Marc E. Fiucynski, Przemyslaw Pardyak, and Brian N. Bershad. Safe dynamic linking in an extensible operating system. In Workshop on Compiler Support for System Software, Tucson, Arizona, February 1996.
• 22: Marvin Solomon, Type definitions with parameters, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.31-38, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512765]
• 23: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, 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
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Languages