TR-2007-10
A Type System for Recursive Modules
Derek Dreyer. 20 July, 2007.
Communicated by Dave MacQueen.
Abstract
There has been much work in recent years on extending ML with
recursive modules. One of the most difficult problems in the
development of such an extension is the double vision problem,
which concerns the interaction of recursion and data abstraction. In
previous work, I defined a type system called RTG, which solves the
double vision problem at the level of a System-F-style core calculus.
In this paper, I scale the ideas and techniques of RTG to the level of
a recursive ML-style module calculus called RMC, thus establishing
that no tradeoff between data abstraction and recursive modules is
necessary. First, I describe RMC's typing rules for recursive modules
informally and discuss some of the design questions that arose in
developing them. Then, I present the formal semantics of RMC, which
is interesting in its own right. The formalization synthesizes
aspects of both the Definition and the Harper-Stone interpretation of
Standard ML, and includes a novel two-pass algorithm for recursive
module typechecking in which the coherence of the two passes is
emphasized by their representation in terms of the same set of
inference rules.
Original Document
The original document is available in PDF (uploaded 20 July, 2007 by
Dave MacQueen).
