paper on recursive modules

We would like to (belatedly) announce the availability of the following TR at


Comments and suggestions would be greatly appreciated.

-- Derek R. Dreyer, Robert Harper, and Karl Crary

Toward a Practical Type Theory for Recursive Modules

Derek R. Dreyer, Robert Harper, and Karl Crary

March 2001


Module systems for languages with complex type systems, such as
Standard ML, often lack the ability to express mutually recursive type
and function dependencies across module boundaries.  Previous work by
Crary, Harper and Puri set out a type-theoretic foundation for
recursive modules in the context of a phase-distinction calculus for
higher-order modules.  Two constructs were introduced for encoding
recursive modules: a fixed-point module and a recursively dependent
signature.  Unfortunately, the implementations of both constructs
involve the use of equi-recursive type constructors at higher-order
kinds, the equivalence of which is not known to be decidable.

In this paper, we show that the practicality of recursive modules is
not contingent upon that of equi-recursive constructors.  We begin
with the theoretical infrastructure described above and study
precisely how equi-recursiveness is used in the recursive module
constructs, resulting in a clarification and generalization of the
underlying ideas.  We then examine in depth how the recursive module
constructs in the revised type system can serve as the target of
elaboration for a recursive module extension to Standard ML.