Higher Order Modules and the Phase Distinction
Robert Harper, John C. Mitchell, and Eugenio Moggi


In earlier work, we used a typed function calculus, XML, with
dependent types to analyze several aspects of the Standard ML type
system.  In this paper, we introduce a refinement of XML with a clear
compile-time/run-time phase distinction, and a direct compile-time
type checking algorithm.  The calculus uses a finer separation of
types into universes than XML and enforces the phase distinction using
a nonstandard equational theory for module and signature expressions.
While unusual from a type-theoretic point of view, the nonstandard
equational theory arises naturally from the well-known Grothendieck
construction on an indexed category.