Practical Type Theory for Recursive Modules

Derek Dreyer. 31 August, 2006.
Communicated by Robby Findler.


There has been much work in recent years on extending ML with recursive modules. We consider two problems with the typechecking of recursive modules that have proven to be serious stumbling blocks for existing proposals. Both problems involve the interaction of recursion and data abstraction. The first, more fundamental problem is that, inside a recursive module, one may wish to define an abstract data type in a context where a name for the type already exists. We call this the double vision problem because it has the effect that the programmer sees two distinct versions of the same type when they should only see one. The second, more superficial problem is that the use of data abstraction inside recursive modules often requires the programmer to write duplicate signature annotations for no clear reason. We call this the repetitive stress problem.

In this paper, we present a recursive module calculus called RMC that addresses both of these problems. We formalize RMC using an elaboration semantics that translates recursive ML-style modules into an internal module type system. The design of the internal language exploits previous work of ours on a type-theoretic foundation for solving the double vision problem. To remedy the repetitive stress problem, our elaboration algorithm employs a novel form of bidirectional typechecking. Although our approach to elaboration generally follows the framework of Harper and Stone, in certain key details it more closely resembles the Definition of Standard ML. The RMC design thus illustrates a viable hybrid of two approaches to defining ML that are commonly viewed as incompatible.

Original Document

The original document is available in PDF (uploaded 31 August, 2006 by Robby Findler).