Toward a Practical Type Theory for Recursive Modules

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 [5] 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.