A type system for higher-order modules.
We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class values. Our type system harmonizes design elements from previous work, resulting in a simple, economical account of modular programming. The main unifying principle is the treatment of abstraction mechanisms as computational effects. Our language is the first to provide a complete and practical formalization of all of these critical issues in module system design.
Introduction
The design of languages for modular programming is surprisingly
delicate and complex. There is a fundamental tension between
# The ConCert Project is supported by the National Science
Foundation under grant number 0121633: "ITR/SY+SI: Language
Technology for Trustless Software Dissemination".
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. To copy otherwise, to republish, to post on servers or to redistribute
to lists, requires prior specific permission and/or a fee.
POPL'03, January 15-17, 2003, New Orleans, Louisiana, USA.
ACM 1-58113-628-5/03/0001 .$5.00
the desire to separate program components into relatively independent
parts and the need to integrate these parts to form a coherent
whole. To some extent the design of modularity mechanisms
is independent of the underlying language [17], but to a large extent
the two are inseparable. For example, languages with poly-
morphism, generics, or type abstraction require far more complex
module mechanisms than those without them.
Much work has been devoted to the design of modular programming
languages. Early work on CLU [19] and the Modula family
of languages [34, 2] has been particularly influential. Much effort
has gone into the design of modular programming mechanisms for
the ML family of languages, notably Standard ML [23] and Objective
Caml [27]. Numerous extensions and variations of these
designs have been considered in the literature [21, 18, 28, 31, 5].
Despite (or perhaps because of) these substantial efforts, the field
has remained somewhat fragmented, with no clear unifying theory
of modularity having yet emerged. Several competing designs have
been proposed, often seemingly at odds with one another. These
decisions are as often motivated by pragmatic considerations, such
as engineering a useful implementation, as by more fundamental
considerations, such as the semantics of type abstraction. The relationship
between these design decisions is not completely clear, nor
is there a clear account of the trade-offs between them, or whether
they can be coherently combined into a single design.
The goal of this paper is to provide a simple, unified formalism
for modular programming that consolidates and elucidates much of
the work mentioned above. Building on a substantial and growing
body of work on type-theoretic accounts of language structure, we
propose a type theory for higher-order program modules that harmonizes
and enriches these designs and that would be suitable as a
foundation for the next generation of modular languages.
1.1 Design Issues
Before describing the main technical features of our language, it is
useful to review some of the central issues in the design of module
systems for ML. These issues extend to any language of similar
expressive power, though some of the trade-offs may be different
for different languages.
Controlled Abstraction Modularity is achieved by using signatures
(interfaces) to mediate access between program components.
The role of a signature is to allow the programmer to "hide" type
information selectively. The mechanism for controlling type propagation
is translucency [11, 14], with transparency and opacity as
limiting cases.
Phase Separation ML-like module systems enjoy a phase separation
property [12] stating that every module is separable into a
static part, consisting of type information, and a dynamic part, consisting
of executable code. To obtain fully expressive higher-order
modules and to support abstraction, it is essential to build this phase
separation principle into the definition of type equivalence.
Generativity MacQueen coined the term generativity for the
creation of "new" types corresponding to run-time instances of
an abstraction. For example, we may wish to define a functor
SymbolTable that, given some parameters, creates a new symbol
table. It is natural for the symbol table module to export an abstract
type of symbols that are dynamically created by insertion and used
for subsequent retrieval. To preclude using the symbols from one
symbol table to index another, generativity is essential-each instance
of the hash table must yield a "new" symbol type, distinct
from all others, even when applied twice to the same parameters.
Separate Compilation One goal of module system design is to
support separate compilation [14]. This is achieved by ensuring
that all interactions among modules are mediated by interfaces that
capture all of the information known to the clients of separately-
compiled modules.
Principal Signatures The principal, or most expressive, signature
for a module captures all that is known about that module during
type checking. It may be used as a proxy for that module for
purposes of separate compilation. Many type checking algorithms,
including the one given in this paper, compute principal signatures
for modules.
Modules as First-Class Values Modules in ML are "second-
class" in the sense that they cannot be computed as the results of
ordinary run-time computation. It can be useful to treat a module
as a first-class value that can be stored into a data structure, or
passed as an ordinary function argument or result [11, 24].
Hidden Types Introducing a local, or "hidden", abstract type
within a scope requires that the types of the externally visible components
avoid mention of the abstract type. This avoidance problem
is often a stumbling block for module system design, since in most
expressive languages there is no "best" way to avoid a type variable
1.2 A Type System for Modules
The type system proposed here takes into account all of these design
issues. It consolidates and harmonizes design elements that were
previously seen as disparate into a single framework. For example,
rather than regard generativity of abstract types as an alternative to
non-generative types, we make both mechanisms available in the
language. We support both generative and applicative functors, admit
translucent signatures, support separate compilation, and are
able to accommodate modules as first-class values [24, 29].
Generality is achieved not by a simple accumulation of features,
but rather by isolating a few key mechanisms that, when com-
bined, yield a flexible, expressive, and implementable type system
for modules. Specifically, the following mechanisms are crucial.
Singletons Propagation of type sharing is handled by singleton
signatures, a variant of Aspinall's and Stone and Harper's singleton
kinds [33, 32, 1]. Singletons provide a simple, orthogonal treatment
of sharing that captures the full equational theory of types in
a higher-order module system with subtyping. No previous module
system has provided both abstraction and the full equational theory
supported by singletons, 1 and consequently none has provided
optimal propagation of type information.
Static Module Equivalence The semantics of singleton signatures
is dependent on a (compile-time) notion of equivalence of
modules. To ensure that the phase distinction is respected, we
define module equivalence to mean "equivalence of static compo-
nents," ignoring all run-time aspects.
Subtyping Signature subtyping is used to model "forgetting"
type sharing, an essential part of signature matching. The coercive
aspects of signature matching (dropping of fields and specialization
of polymorphic values) are omitted here, since the required coercions
are definable in the language.
Purity and Impurity Our type system classifies module expressions
into pure (effect-free) and impure (effectful) forms. To ensure
proper enforcement of abstraction, impure modules are incomparable
(may not be compared for equality with any other module)
and non-projectible (may not have type components projected from
them). It follows that impure modules are also non-substitutable
(may not be substituted for a module variable in a signature).
Abstraction and Sealing Modules that are sealed with a signature
to impose type abstraction [11] are regarded as impure. In other
words, sealing is regarded as a pro forma computational effect. This
is consistent with the informal idea that generativity involves the
generation of new types at run time. Moreover, this ensures that
sealed modules are incomparable and non-projectible, which is sufficient
to ensure the proper semantics of type abstraction.
Totality and Partiality Functors are l-abstractions at the level of
modules. A functor whose body is pure is said to be total; otherwise
it is partial. It follows that the application of a pure, total functor to
a pure argument is pure, whereas the application of a pure, partial
functor to a pure argument is impure. Partial functors are naturally
generative, meaning that the abstract types in its result are "new"
for each instance; total functors are applicative, meaning that equal
arguments yield equal types in the result. Generative functors are
obtained without resort to "generative stamps" [23, 21].
Weak and Strong Sealing Since sealing induces a computational
effect, only partial functors may contain sealed sub-
structures; this significantly weakens the utility of total functors.
To overcome this limitation we distinguish two forms of effect,
static and dynamic, and two forms of sealing, weak and strong.
Weak sealing induces a static effect, which we think of as occurring
once during type checking; strong sealing induces a dynamic
effect, which we think of as occurring during execution. Dynamic
effects induce partiality, static effects preserve totality.
Existential Signatures In a manner similar to Shao [31], our
type system is carefully crafted to circumvent the avoidance prob-
lem, so that every module enjoys a principal signature. However,
this requires imposing restrictions on the programmer. To lift these
restrictions, we propose the use of existential signatures to provide
principal signatures where none would otherwise exist. We show
that these existential signatures are type-theoretically ill-behaved in
1 Typically the omitted equations are not missed because restrictions
to named form or valuability prevent programmers from writing
code whose typeability would depend on those equations in the
first place [4].
terms e
signatures s
modules
let s =M 1 in
M:>s | M::s
contexts G ::= . | G,s:s

Figure

1. Syntax
general, so, we restrict their use to a well-behaved setting. In the
style of Harper and Stone [13], we propose the use of an elaboration
algorithm from an external language that may incur the avoidance
problem, into our type system, which does not.
Packaged Modules Modules in our system are "second-class" in
the sense that the language of modules is separate from the language
of terms. However, following Mitchell et al. [24] and Russo [29],
we provide a way of packaging a module as a first-class value. In
prior work, such packaged modules are typically given an existential
type, whose closed-scope elimination construct can make for
awkward programming. Instead, our account of type generativity
allows us to employ a more natural, open-scope elimination con-
struct, whereby unpackaging a packaged module engenders a dynamic
effect.
While these features combine naturally to form a very general language
for modular programming, they would be of little use in
the absence of a practical implementation strategy. Some previous
attempts have encountered difficulties with undecidability [11]
or incompleteness of type checking [27]. In contrast, our formalism
leads to a practical, implementable programming language.
The rest of this paper is structured as follows: In Section 2 we
present our core type system for higher-order modules, including
the intuition behind its design and a brief description of the decidable
typechecking algorithm. In Section 3 we discuss the programming
importance of having both weak and strong forms of
sealing. In Section 4 we explain the avoidance problem and how
it can be circumvented using an elaboration algorithm. In Section 5
we present a very simple, orthogonal extension of our core system
to provide support for packaging modules as first-class values. Fi-
nally, in Section 6 we compare our system with related work and in
Section 7 we conclude.
Technical Development
We begin our technical development by presenting the syntax of
our language in Figure 1. Our language consists of four syntactic
classes: terms, types, modules, and signatures (which serve as
the types of modules). The language does not explicitly include
higher-order type constructors or kinds (which ordinarily serve as
constructors' types); in our language the roles of constructors and
kinds are subsumed by modules and signatures. Contexts bind module
variables (s) to signatures.
As usual, we consider alpha-equivalent expressions to be identical.
We write the capture-avoiding substitution of M for s in an expression
Types There are three basic types in our language. The product
standard. The function type, Ps:s.t, is the type of
functions that accept a module argument s of signature s and return
a value of type t (possibly containing s). As usual, if s does not
appear free in t, we write Ps:s.t as s#t. (This convention is used
for the dependent products in the signature class as well.) Finally,
when M is a module containing exactly one type (which is to say
that M has the signature [[T ]]), that type is extracted by Typ M. A
full-featured language would support a variety of additional types
as well.
Terms The term language contains the natural introduction and
elimination constructs for recursive functions and products. In ad-
dition, when M is a module containing exactly one value (which is
to say that M has the signature [[t]], for some type t), that value is
extracted by Val M. When f does not appear free in e, we write
fix f (s:s):t.e as Ls:s.e.
The conventional forms of functions and polymorphic function are
built from module functions. Ordinary functions are built using
modules containing a single value:
and polymorphic functions are built using modules containing a single
type:
et
Signatures There are seven basic signatures in our language. The
atomic signature [[T is the type of an atomic module containing a
single type, and the atomic signature [[t]] is the type of an atomic
module containing a single term. The atomic modules are written
[t] and [e : t], respectively. (We omit the type label ": t" from atomic
modules when it is clear from context.) The trivial atomic
signature 1 is the type of the trivial atomic module #.
The functor signatures P tot s:s 1 .s 2 and P par s:s 1 .s 2 express the
type of functors that accept an argument of signature s 1 and return
a result of signature s 2 (possibly containing s). The reason for two
different P signatures is to distinguish between total and partial
functors, which we discuss in detail below. For convenience, we
will take P (without a superscript) to be synonymous with P tot .
When s does not appear free in s 2 , we write Ps:s 1 .s 2 as s 1 #s 2 .
The structure signature Ss:s 1 .s 2 is the type of a pair of modules
where the left-hand component has signature s 1 and the right-hand
component has signature s 2 , in which s refers to the left-hand com-
ponent. As usual, when s does not appear free in s 2 , we write
The singleton signature s(M) is used to express type sharing infor-
mation. It classifies modules that have signature [[T are statically
equivalent to M. Two modules are considered statically equivalent
if they are equal modulo term components; that is, type fields
must agree but term fields may differ. Singletons at signatures other
than [[T are not provided primitively because they can be defined
using the basic singleton, as described by Stone and Harper [33].
The definition of s s (M) (the signature containing only modules
equal to M at signature s) is given in Figure 5.
signature
sig
type s
type u
val
end . is compiled as .

Figure

2. ML Signature Example
Modules The module syntax contains module variables (s), the
atomic modules, and the usual introduction and elimination constructs
for P and S signatures, except that S modules are introduced
by #, in which s stands for M 1 and may appear free in
does not appear free in M 2 , the "s =" is omitted.)
No introduction or elimination constructs are provided for singleton
signatures. Singletons are introduced and eliminated by rules in
the static semantics; if M is judged equivalent to M # in s, then M
belongs to s s (M # ), and vice versa.
The remaining module constructs are strong sealing, written
M:>s, and weak sealing, written M::s. When a module is sealed
either strongly or weakly, the result is opaque. By opaque we mean
that no client of the module may depend on any details of the implementation
of M other than what is exposed by the signature s. The
distinction between strong and weak sealing is discussed in detail
below.
Although higher-order type constructors do not appear explicitly
in our language, they are faithfully represented in our language by
unsealed modules containing only type components. For example,
the kind (T #T )#T is represented by the signature ([[T
]]; and the constructor la:(T #T ).(int -aint) is represented
by the module ls:([[T
Examples of how ML-style signatures and structures may be expressed
in our language appear in Figures 2 and 3.
Comparability and Projectibility Two closely related issues are
crucial to the design of a module system supporting type abstraction

1. When can a module be compared for equivalence with another
module?
2. When can a type component be projected from a module and
used as a type?
We say that a module is comparable iff it can be compared for
equivalence with another module, and that a module is projectible
its type components may be projected and used as type expres-
sions. (In the literature most presentations emphasize projectibil-
ity [11, 14, 15].)
structure
struct
structure struct
type string
val
val
end . is compiled as .

Figure

3. ML Structure Example
A simple analysis of the properties of comparability and projectibil-
ity suggests that they are closely related. Suppose that M is a pro-
jectible module with signature [[T ]], so that Typ M is a type. Since
type equality is an equivalence relation, this type may be compared
with any other, in particular, Typ M # for another projectible module
M # of the same signature. But since Typ M and Typ M # fully
determine M, we are, in effect, comparing M with M # for equiva-
lence. This suggests that projectible modules be regarded as comparable
for type checking purposes. Conversely, if M is a comparable
module, then by extensionality M should be equivalent to [Typ M],
which is only sensible if M is also projectible.
Purity and Impurity The design of our module system rests on
the semantic notions of purity and impurity induced by computational
effects. To motivate the design, first recall that in a first-class
module system such as Harper and Lillibridge's [11] there can be
"impure" module expressions that yield distinct type components
each time they are evaluated. For example, a module expression
might consult the state of the world, yielding a different module
for each outcome of the test. The type components of such a
module are not statically well-determined, and hence should not be
admitted as type expressions at all, much less compared for equiv-
alence. On the other hand, even in such a general framework, pure
(effect-free) modules may be safely regarded as both comparable
and projectible.
In a second-class module system such examples are not, in fact,
expressible, but we will nevertheless find it useful to classify modules
according to their purity. 2 This classification is semantic, in
the sense of being defined by judgments of the calculus, rather than
syntactic, in the sense of being determined solely by the form of
expression. Such a semantic approach is important for a correct
account of type abstraction in a full-featured module language.
The axiomatization of purity and impurity in our system is based on
a set of rules that takes account of the types of expressions, as well
as their syntactic forms. The type system is conservative in that
it "assumes the worst" of an impure module expression, ruling it
2 Moreover, in Section 5 we will introduce the means to re-create
these examples in our setting, making essential use of the same classification
system.
incomparable and non-projectible, even when its type components
are in fact statically well-determined. As we will see shortly, this is
important for enforcing type abstraction, as well as ensuring soundness
in the presence of first-class modules. In addition, since it is
sound to do so, we deem all pure module expressions to be comparable
and projectible. That is, to be as permissive as possible without
violating soundness or abstraction, we identify comparability
and projectibility with purity. Finally, note that a module is judged
pure based on whether its type components are well-determined,
which is independent of whether any term components have computational
effects.
In the literature different accounts of higher-order modules provide
different classes of pure modules. For example, in Harper and Lil-
libridge's first-class module system [11], only syntactic values are
considered pure. In Leroy's second-class module calculi [14, 15],
purity is limited to the syntactic category of paths. In Harper et al.'s
early "phase-distinction" calculus [12] all modules are deemed to
be pure, but no means of abstraction is provided.
Abstraction via Sealing The principal means for defining abstract
types is sealing, written M:>s. Sealing M with s prevents
any client of M from depending on the identities of any type
components specified opaquely-with signature [[T
From the point of view of module equivalence,
this means that a sealed module should be considered incompara-
ble. To see this, suppose that regarded as
comparable. Presumably, M could not be deemed equivalent to
since their underlying type components are
different. However, since module equivalence is reflexive, if M
is comparable, then M must be deemed equivalent to itself. This
would mean that the type system would distinguish two opaque
modules based on their underlying implementation, a violation of
type abstraction.
A significant advantage of our judgmental approach to purity is that
it affords a natural means of ensuring that a sealed module is in-
comparable, namely to judge it impure. This amounts to regarding
sealing as a pro forma run-time effect, even though no actual effect
occurs at execution time. Not only does this ensure that abstraction
violations such as the one just illustrated are ruled out, but we will
also show in Section 3 that doing so allows the type system to track
the run-time "generation" of "new" types.
Applicative and Generative Functors Functors in Standard ML
are generative in the sense that each abstract type in the result of
the functor is "generated afresh" for each instance of the functor,
regardless of whether or not the arguments in each instance are
equivalent. Functors in Objective Caml, however, are applicative
in the sense that they preserve equivalence: if applied to equivalent
arguments, they yield equivalent results. In particular, the abstract
types in the result of a functor are the same for any two applications
to the same argument.
Continuing the analogy with computational effects, we will deem
any functor whose body is pure to be total, otherwise partial. The
application of a pure, total functor to a pure argument is pure, and
hence comparable. Total functors are applicative in the sense that
the application of a pure total functor to two equivalent pure modules
yields equivalent pure modules, because the applications are
pure, and hence comparable. Partial functors, on the other hand,
always yield impure modules when applied. Therefore they do not
respect equivalence of arguments (because the results, being im-
pure, are not even comparable), ensuring that each instance yields
a distinct result.
We distinguish the signatures of total (applicative) and partial (gen-
erative) functors. Total functors have P signatures, whereas partial
functors have P par signatures. The subtyping relation is defined so
that every total functor may be regarded (degenerately) as a partial
functor.
Weak and Strong Sealing In our system we identify applicative
functors with total ones, and generative functors with partial ones.
To make this work, however, we must refine the notion of effect.
For if sealing is regarded as inducing a run-time effect, then it is
impossible to employ abstraction within the body of a total func-
tor, for to do so renders the body impure. (We may seal the entire
functor with a total functor signature to impose abstraction, but this
only ensures that the exported types of the functor are held abstract
in any clients of that functor. It does not permit a substructure in
the body of the functor to be held abstract in both the clients of the
functor and in the remainder of the functor body.)
The solution is to distinguish two forms of sealing-strong, written
M:>s as before, and weak, written M::s. Both impose abstraction
in the sense of limiting type propagation to what is explicitly
specified in the ascribed signature by regarding both forms of sealing
as inducing impurity. However, to support a useful class of
applicative functors, we further distinguish between static and dynamic
effects. Weak sealing induces a static effect, whereas strong
sealing induces dynamic effect.
The significance of this distinction lies in the definition of total and
partial functors. A functor whose body involves a dynamic effect
(i.e., is dynamically impure), is ruled partial, and hence generative.
Thus strong sealing within a functor body induces generativity of
that functor. A functor whose body is either pure, or involves only
a static effect (i.e., is dynamically pure), is ruled total, and hence
applicative. This ensures that applicative functors may use abstraction
within their bodies without incurring generative behavior. The
methodological importance of this distinction is discussed in Section
3.
A dynamic effect may be thought of as one that occurs during exe-
cution, whereas a static effect is one that occurs during type check-
ing. Dynamic effects are suspended inside of a l-abstraction, so
functor abstractions are dynamically pure. However, when applied,
the dynamic effects inside the functor are released, so that the application
is dynamically impure. On the other hand, static effects
occur during type checking, and hence are not suspended by l-
abstraction, nor released by application.
Formalization The typing judgment for our system is written
purity. The classifier k is drawn
from the following four-point lattice:
The point P indicates that M is pure (and hence comparable and pro-
jectible), D indicates dynamic purity, S indicates static purity, and
W indicates well-formedness only (no purity information). Hence,
our purity judgment. It will prove to be convenient
in our typing rules to exploit the ordering (written #), meets (#),
and joins (#) of this lattice, where P is taken as the bottom and W
is taken as the top. We also sometimes find it convenient to use
the notation P d s:s 1 .s 2 for a functor signature that is either total or
partial depending on whether

Figure

4. Key Typing Rules
Some key rules are summarized in Figure 4. Pure modules are dynamically
pure and statically pure, and each of those are at least
well-formed (rule 1). Strongly sealed modules are neither statically
nor dynamically pure (2); weakly sealed modules are not statically
pure, but are dynamically pure if their body is (3). Applicative
functors must have dynamically pure bodies (5); generative functors
have no restriction (6). Applicative functors may be used as
generative ones (7). Variables are pure (4), and lambdas are dynamically
pure (5 and 6). The application of an applicative functor
is as pure as the functor itself (8), but the application of a generative
functor is at best statically pure (9). Finally, the purity of a module
is preserved by signature subsumption (12). The complete set of
typing rules is given in Appendix A.
The rules for functor application (rules 8 and require that the
functor argument be pure. This is because the functor argument is
substituted into the functor's codomain to produce the result signa-
ture, and the substitution of impure modules for variables (which
are always pure) can turn well-formed signatures into ill-formed
ones (for example, [Typ s] becomes ill-formed if an impure module
is substituted for s). (An alternative rule proposed by Harper
and Lillibridge [11] resolves this issue, but induces the avoidance
problem, as we discuss in Section 4.) Therefore, when a functor
is to be applied to an impure argument, that argument must first be
bound to a variable, which is pure. Similarly, projection of the second
component of a pair is restricted to pure pairs (rule 11), but no
such restriction need be made for projection of the first component
(rule 10), since no substitution is involved.
Static Equivalence In the foregoing discussion we have frequently
made reference to a notion of module equivalence, without
specifying what this means. A key design decision for a module calculus
is to define when two comparable modules are to be deemed
equivalent. Different module systems arise from different notions
of equivalence.
If a pure module has signature [[T ]], it is possible to extract the
type component from it. Type checking depends essentially on
the matter of which types are equal, so we must consider when
Typ M is equal to Typ M # . The simplest answer would be to regard
exactly when the modules M and M # are equal.
But this is too naive because we cannot in general determine when
two modules are equal. Suppose F :
but the latter equality is undecidable
in general.
A characteristic feature of second class module systems is that they
respect the phase distinction [12] between compile-time and run-time
computation. This property of a module system states that type
equivalence must be decidable independently of term equivalence.
This should be intuitively plausible, since a second-class module
system provides no means by which a type component of a module
can depend on a term component. (This is not happenstance, but
the result of careful design. We will see in Section 5 that the matter
is more subtle than it appears.)
Based on this principle, we define module equivalence to be "equiv-
alence for type checking purposes", or static equivalence. Roughly
speaking, two modules are deemed to be equivalent whenever they
agree on their corresponding type components. 3
We write our module equivalence judgment as G # M
The rules for static equivalence of atomic modules are the expected
ones. Atomic type components must be equal, but atomic term
components need not be:
Since the generative production of new types in a generative functor
is notionally a dynamic operation, generative functors have no static
components to compare. Thus, pure generative functors are always
statically equivalent, just as atomic term modules are:
The complete set of equivalence rules is given in Appendix A.
As an aside, this discussion of module equivalence refutes the misconception
that first-class modules are more general than second-class
modules. In fact, the expressiveness of first- and second-class
modules is incomparable. First-class modules have the obvious advantage
that they are first-class. However, since the type components
of a first-class module can depend on run-time computations,
it is impossible to get by with static module equivalence and one
3 The phase distinction calculus of Harper, et al. [12] includes
"non-standard" equality rules for phase-splitting modules M into
structures #M stat , M dyn # consisting of a static component M stat and a
dynamic component M dyn . Our static equivalence M # =M # amounts
to saying M stat =M #
stat in their system. However, we do not identify
functors with structures, as they do.
must use dynamic equivalence instead (in other words, one cannot
phase-split modules as in Harper et al. [12]). Consequently,
first-class modules cannot propagate as much type information as
second-class modules can.
Singleton Signatures Type sharing information is expressed in
our language using singleton signatures [33], a derivative of translucent
sums [11, 14, 18]. (An illustration of the use of singleton
signatures to express type sharing appears in Figure 2.) The type
system allows the deduction of equivalences from membership in
singleton signatures, and vice versa, and also allows the forgetting
of singleton information using the subsignature relation:
When deductions follow using primitive rules of the
type system (since s [[T
tures, they follow from the definitions given in Figure 5.
Beyond expressing sharing, singletons are useful for "selfifica-
tion" [11]. For instance, if s is a variable bound with the signature
can be given the fully transparent signature s(s). This fact is
essential to the existence of principal signatures in our type checking
algorithm. Note that since singleton signatures express static
equivalence information, the formation of singleton signatures is
restricted to pure modules. Thus, only pure modules can be selfi-
fied (as in Harper and Lillibridge [11] and Leroy [14]).
Singleton signatures complicate equivalence checking, since equivalence
can depend on context. For example, ls:[[T ]].[int] and
ls:[[T ]].s are obviously inequivalent at signature [[T
ever, using subsignatures, they can also be given the signature
and at that signature they are equivalent, since they
return the same result when given the only permissible argument,
[int].
As this example illustrates, the context sensitivity of equivalence
provides more type equalities than would hold if equivalence were
strictly context insensitive, thereby allowing the propagation of additional
type information. For example,
]], then the types Typ(F(ls:[[T ]].[int])) and Typ (F(ls:[[T ]].s))
are equal, which could not be the case under a context-insensitive
regime.
A subtle technical point arises in the use of the higher-order
singletons defined in Figure 5. Suppose F :
which intuitively contains the modules
equivalent to F: those that take members of F's domain and
return the same thing that F does. Formally speaking, however, the
canonical member of this signature is not F but its eta-expansion
ls:[[T ]].Fs. In fact, it is not obvious that F belongs to s [[T ]]#[[T
To ensure that F belongs to its singleton signature, our type system
(following Stone and Harper [33]) includes the extensional typing
rule:
Using this rule, F belongs to Ps:[[T ]].s(F s) because it is a function
and because Fs belongs to s(F s). A similar extensional typing
rule is provided for products. It is possible that the need for these
s
(Ms)

Figure

5. Singletons at Higher Signatures
rules could be avoided by making higher-order singletons primitive,
but we have not explored the meta-theoretic implications of such a
change.
Since a module with a (higher-order) singleton signature is fully
transparent, it is obviously projectible and comparable, and hence
could be judged to be pure, even if it would otherwise be classified
as impure. This is an instance of the general problem of recognizing
that "benign effects" need not disturb purity. Since purity is a judgment
in our framework, we could readily incorporate extensions to
capture such situations, but we do not pursue the matter here.
Type Checking Our type system enjoys a sound, complete, and
effective type checking algorithm. Our algorithm comes in three
main parts: first, an algorithm for synthesizing the principal (i.e.,
minimal) signature of a module; second, an algorithm for checking
subsignature relationships; and third, an algorithm for deciding
equivalence of modules and of types.
Module typechecking then proceeds in the usual manner, by synthesizing
the principal signature of a module and then checking
that it is a subsignature of the intended signature. The signature
synthesis algorithm is given in Appendix B, and its correctness theorems
are stated below. The main judgment of signature synthesis
is G # k M # s, which states that M's principal signature is s and
M's purity is inferred to be k.
Subsignature checking is syntax-directed and easy to do, given an
algorithm for checking module equivalence; module equivalence
arises when two singleton signatures are compared for the subsigna-
ture relation. The equivalence algorithm is closely based on Stone
and Harper's algorithm [33] for type constructor equivalence in the
presence of singleton kinds. Space considerations preclude further
discussion of this algorithm here. Full details of all these algorithms
and proofs appear in the companion technical report [7].
THEOREM 2.1 (SOUNDNESS). If G
THEOREM 2.2 (COMPLETENESS). If G
Note that since the synthesis algorithm is deterministic, it follows
from Theorem 2.2 that principal signatures exist. Finally, since our
synthesis algorithm, for convenience, is presented in terms of inference
rules, we require one more result stating that it really is an
algorithm:
THEOREM 2.3 (EFFECTIVENESS). For any G and M, it is decidable
whether there exist s and k such that G # k M # s.
signature SYMBOL
sig
type symbol
val string to symbol : string -> symbol
val symbol to string : symbol -> string
val
functor SymbolTableFun () :> SYMBOL
struct
val table : string array =
(* allocate internal hash table *)
Array.array (initial size, NONE)
fun string to symbol
(* lookup (or insert) x *) .
fun symbol to string
(case Array.sub (table, n) of
| NONE => raise (Fail "bad symbol"))
structure

Figure

6. Strong Sealing Example
3 Strong and Weak Sealing
Generativity is essential for providing the necessary degree of abstraction
in the presence of effects. When a module has side-effects,
such as the allocation of storage, abstraction may demand that types
be generated in correspondence to storage allocation, in order to ensure
that elements of those types relate to the local store and not the
store of another instance.
Consider, for example, the symbol table example given in Figure 6.
A symbol table contains an abstract type symbol, operations for in-
terconverting symbols and strings, and an equality test (presumably
faster than that available for strings). The implementation creates
an internal hash table and defines symbols to be indices into that
internal table.
The intention of this implementation is that the Fail exception
never be raised. However, this depends on the generativity of
the symbol type. If another instance, SymbolTable2, is created,
and the types SymbolTable.symbol and SymbolTable2.symbol
are considered equal, then SymbolTable could be asked to
interpret indices into SymbolTable2's table, thereby causing
failure. Thus, it is essential that SymbolTable.symbol and
SymbolTable2.symbol be considered unequal.
The symbol table example demonstrates the importance of strong
sealing for encoding generative abstract types in stateful modules.
Generativity is not necessary, however, for purely functional mod-
ules. Leroy [15] gives several examples of such modules as motivation
for the adoption of applicative functors. For instance, one
may wish to implement persistent sets using ordered lists. Figure 7
signature
sig
type elem
val compare : elem * elem -> order
signature persistent sets *)
sig
type elem
type set
val empty : set
val insert : elem * set -> set
struct
list
structure struct
val
structure
structure

Figure

7. Weak Sealing Example
exhibits a purely functional SetFun functor, which is parameterized
over an ordered element type, and whose implementation of
the abstract set type is sealed. When SetFun is instantiated multiple
times-e.g., in different client modules-with the same element
type, it is useful for the resulting abstract set types to be seen as
interchangeable.
In our system, SetFun is made applicative, but still opaque,
by weakly sealing its body. Specifically, IntSet1.set and
IntSet2.set are both equivalent to SetFun(IntOrd).set. This
type is well-formed because SetFun has an applicative functor sig-
nature, and SetFun and IntOrd, being variables, are both pure.
Recall that a functor containing weak sealing is impure and must
be bound to a variable before it can be used applicatively.
The astute reader may notice that weak sealing is not truly necessary
in the SetFun example. In fact, one can achieve the same effect
as the code in Figure 7 by leaving the body of the functor unsealed
and (strongly) sealing the functor itself with an applicative functor
signature before binding it to SetFun. This is the technique employed
by Shao [31] for encoding applicative functors, as his system
lacks an analogue of weak sealing. A failing of this approach
is that it only works if the functor body is fully transparent-in the
absence of weak sealing, any opaque substructures would have to
be strongly sealed, preventing the functor from being given an applicative
signature.
The best examples of the need for opaque substructures in applicative
functors are provided by the interpretation of ML datatype's
as abstract types [13]. In both Standard ML and Caml, datatype's
are opaque in the sense that their representation as recursive sum
types is not exposed, and thus distinct instances of the same
datatype declaration create distinct types. Standard ML and
Caml differ, however, on whether datatype's are generative. In
the presence of applicative functors (which are absent from Standard
ML) there is excellent reason for datatype's not to be
generative-namely, that a generative interpretation would prevent
datatype's from appearing in the bodies of applicative functors.
This would severely diminish the utility of applicative functors, particularly
since in ML recursive types are provided only through the
datatype mechanism. For example, an implementation of SetFun
with splay trees, using a datatype declaration to define the tree
type, would require the use of weak sealing.
For these reasons, strong sealing is no substitute for weak sealing.
Neither is weak sealing a substitute for strong. As Leroy [15] ob-
served, in functor-free code, generativity can be simulated by what
we call weak sealing. (This can be seen in our framework by observing
that dynamic purity provides no extra privileges in the absence
of functors.) With functors, however, strong sealing is necessary
to provide true generativity. Nevertheless, it is worth noting
that strong sealing is definable in terms of other constructs in our
language, while weak sealing is not. In particular, we can define
strong sealing, using a combination of weak sealing and generative
functor application, as follows:
The existence of this encoding does not diminish the importance
of strong sealing, which we have made primitive in our language
regardless.
4 The Avoidance Problem
The rules of our type system (particularly rules 8, 9, and 11 from

Figure

are careful to ensure that substituted modules are always
pure, at the expense of requiring that functor and second-projection
arguments are pure. This is necessary because the result of substituting
an impure module into a well-formed signature can be ill-
formed. Thus, to apply a functor to an impure argument, one must
let-bind the argument and apply the functor to the resulting (pure)
variable.
A similar restriction is imposed by Shao [31], but Harper and Lillibridge
[11] propose an alternative that softens the restriction. Harper
and Lillibridge's proposal (expressed in our terms) is to include a
non-dependent typing rule without a purity restriction:
When M 2 is pure, this rule carries the same force as our dependent
rule, by exploiting singleton signatures and the contravariance of
functor signatures:
When M 2 is impure, this rule is more expressive than our typing
rule, because the application can still occur. However, to exploit
this rule, the type checker must find a non-dependent supersignature
that is suitable for application to M 2 .
The avoidance problem [9, 18] is that there is no "best" way to do
so. For example, consider the signature:
To obtain a supersignature of s avoiding the variable s, we must
forget that the first component is a constant function, and therefore
we can only say that the second component is equal to the first
component's result on some particular argument. Thus, for any type
t, we may promote s to the supersignature:
This gives us an infinite array of choices. Any of these choices is
superior to the obvious ([[T but none of them is comparable
to any other, since F is abstract. Thus, there is no minimal
supersignature of s avoiding s. The absence of minimal signatures
is a problem, because it means that there is no obvious way to perform
type checking.
In our type system, we circumvent the avoidance problem by requiring
that the arguments of functor application and second-projection
be pure (thereby eliminating any need to find non-dependent super-
signatures), and provide a let construct so that such operations can
still be applied to impure modules. We have shown that, as a result,
our type theory does enjoy principal signatures.
To achieve this, however, our let construct must be labeled with its
result signature (not mentioning the variable being bound), for otherwise
the avoidance problem re-arises. This essentially requires
that every functor application or projection involving an impure argument
be labelled with its result signature as well, leading to potentially
unacceptable syntactic overhead in practice. Fortunately,
programs can be systematically rewritten to avoid this problem, as
we describe next.
4.1 Elaboration and Existential Signatures
Consider the unannotated let expression let
pure, then the let expression can
be given the minimal signature s 2 (M 1 ). Otherwise, we are left with
the variable s leaving scope, but no minimal supersignature of s 2
not mentioning s. However, if we rewrite the let expression as the
#, then we may give it the signature Ss:s 1 .s 2
and no avoidance problem arises. Similarly, the functor application
F(M) with can be rewritten as
#s =M,F(s)# and given signature Ss:s 1 .s 2 .
Following Harper and Stone [13], we propose the use of an elaboration
algorithm to systematize these rewritings. This elaborator takes
code written in an external language that supports unannotated let's,
as well as impure functor application and second-projection, and
produces code written in our type system. Since the elaborator
rewrites modules in a manner that changes their signatures, it also
must take responsibility for converting those modules back to their
expected signature wherever required. This means that the elabora-
tor must track which pairs are "real" and which have been invented
by the elaborator to circumvent the avoidance problem.
The elaborator does so using the types. When the elaborator invents
a pair to circumvent the avoidance problem, it gives its signature using
an existential # rather than S. In the internal language, #s:s 1 .s 2
means the same thing as Ss:s 1 .s 2 , but the elaborator treats the two
signatures differently: When the elaborator expects (say) a functor
and encounters a Ss:s 1 .s 2 , it generates a type error. However, when
it encounters an #s:s 1 .s 2 , it extracts the s 2 component (the elab-
orator's invariants ensure that it always can do so), looking for the
expected functor. Space considerations preclude further details of
the elaboration algorithm, which appear in the companion technical
report [7].
In a sense, the elaborator solves the avoidance problem by introducing
existential signatures to serve in place of the non-existent
minimal supersignatures not mentioning a variable. In light of this,
a natural question is whether the need for an elaborator could be
eliminated by making existential signatures primitive to the type
system.
One natural way to govern primitive existentials is with the introduction
and elimination rules:
and
With these rules, the avoidance problem could be solved: The least
supersignature of s 2 not mentioning s:s 1 would be #s:s 1 .s 2 (s).
Unfortunately, these rules (particularly the first) make type checking
undecidable. For example, each of the queries
and
(ls:s.[t])
holds if and only if there exists pure s such that the types t[M/s]
and t # [M/s] are equal. Thus, deciding subsignature or equivalence
queries in the presence of existentials would be as hard as higher-order
unification, which is known to be undecidable [10].
4.2 Syntactic Principal Signatures
It has been argued for reasons related to separate compilation that
principal signatures should be expressible in the syntax available to
the programmer. This provides the strongest support for separate
compilation, because a programmer can break a program at any
point and write an interface that expresses all the information the
compiler could have determined at that point. Such strong support
does not appear to be vital in practice, since systems such as Objective
Caml and Standard ML of New Jersey's higher-order modules
have been used successfully for some time without principal signatures
at all, but it is nevertheless a desirable property.
Our type system (i.e., the internal language) does provide syntactic
principal signatures, since principal signatures exist, and all the
syntax is available to the programmer. However, the elaborator's
external language does not provide syntax for the existential signatures
that can appear in elaborator signatures, which should be
thought of as the principal signatures of external modules. Thus,
we can say that our basic type system provides syntactic principal
signatures, but our external language does not.
In an external language where the programmer is permitted to write
existential signatures, elaborating code such as:
requires the elaborator to decide whether M can be coerced to belong
to #s:s 1 .s 2 , which in turn requires the elaborator to produce a
Determining whether any such M #
exists requires the elaborator to solve an undecidable higher-order
unification problem: if s
only if t[M # /s] and t # [M # /s] are equal.
Thus, to allow programmer-specified existential signatures in the
greatest possible generality would make elaboration undecidable.
Partial measures may be possible, but we will not discuss any here.
Packaging Modules as First-Class Values
It is desirable for modules to be usable as first-class values. This is
useful to make it possible to choose at run time the most efficient
implementation of a signature for a particular data set (for example,
sparse or dense representations of arrays). However, fully general
first-class modules present difficulties for static typing [18].
One practical approach to modules as first-class values was suggested
by Mitchell, et al. [24], who propose that second-class modules
automatically be wrapped as existential packages [25] to obtain
first-class values. A similar approach to modules as first-class values
is described by Russo and implemented in Moscow ML [29].
This existential-packaging approach to modules as first-class values
is built into our language. We write the type of a packaged module
as #|s|# and the packaging construct as pack M as #|s|#. Elimination
of packaged modules (as for existentials) is performed using
a closed-scope unpacking construct. These may be defined as follows

pack M as #|s|# def
unpack e as s:s in
(Compare the definition of #|s|# with the standard encoding of the
existential type #b.t as #a.(#b.t#a)#a.)
The main limitation of existentially-packaged modules is the
closed-scope elimination construct. It has been observed repeatedly
in the literature [20, 3, 18] that this construct is too restrictive to be
very useful. For one, in "unpack e as s:s in (e # : t)", the result type
t may not mention s. As a consequence, functions over packaged
modules may not be dependent; that is, the result type may not mention
the argument. This deficiency is mitigated in our language by
the ability to write functions over unpackaged, second-class mod-
ules, which can be given the dependent type Ps:s.t(s) instead of
#|s|# t.
Another problem with the closed-scope elimination construct is
that a term of package type cannot be unpacked into a stand-alone
second-class module; it can only be unpacked inside an enclosing
term. As each unpacking of a packaged module creates an abstract
type in a separate scope, packages must be unpacked at a very early
stage to ensure coherence among their clients, leading to "scope
inversions" that are awkward to manage in practice.
What we desire, therefore, is a new module construct of the form
"unpack e as s", which coerces a first-class package e of type #|s|#
back into a second-class module of signature s. The following example
illustrates how adding such a construct carelessly can lead to
unsoundness:
module
module
module
Note that the argument of the functor F is an atomic term module,
so all arguments to F are statically equivalent. If F is given an
applicative signature, then X 1 and X 2 will be deemed equivalent,
even if the original modules M 1 and M 2 are not! Thus, F must be
types t ::= - | #|s|#
terms e ::= - | pack M as #|s|#
modules M ::= - | unpack e as s
pack M as #|s|#|s|#

Figure

8. Packaged Module Extension
deemed generative, which in turn requires that the unpack construct
induce a dynamic effect.
Packaged modules that admit this improved unpacking construct
are not definable in our core language, but they constitute a simple,
orthogonal extension to the type system that does not complicate
type checking. The syntax and typing rules for this extension are
given in Figure 8. Note that the closed-scope unpacking construct
is definable as
Intuitively, unpacking is generative because the module being unpacked
can be an arbitrary term, whose type components may depend
on run-time conditions. In the core system we presented in
Section 2, the generativity induced by strong sealing was merely a
pro forma effect-the language, supporting only second-class mod-
ules, provided no way for the type components of a module to be
actually generated at run time. The type system, however, treats
dynamic effects as if they are all truly dynamic, and thus it scales
easily to handle the real run-time type generation enabled by the
extension in Figure 8.
6 Related Work
Harper, Mitchell and Moggi [12] pioneered the theory of phase sep-
aration, which is fundamental to achieving maximal type propagation
in higher-order module systems. Their non-standard equational
rules, which identify higher-order modules with primitive "phase-
split" ones, are similar in spirit to, though different in detail from,
our notion of static module equivalence. One may view their system
as a subsystem of ours in which there is no sealing mechanism
(and consequently all modules are pure).
MacQueen and Tofte [21] proposed a higher-order module extension
to the original Definition of Standard ML [22], which was implemented
in the Standard ML of New Jersey compiler. Their semantics
involves a two-phase elaboration process, in which higher-order
functors are re-elaborated at each application to take advantage
of additional information about their arguments. This advantage
is balanced by the disadvantage of inhibiting type propagation
in the presence of separate compilation since functors that are compiled
separately from their applications cannot be re-elaborated. A
more thorough comparison is difficult because MacQueen and Tofte
employ a stamp-based semantics, which is difficult to transfer to a
setting.
Focusing on controlled abstraction, but largely neglecting higher-order
modules, Harper and Lillibridge [11] and Leroy [14, 16] introduced
the closely related concepts of translucent sums and manifest
types. These mechanisms served as the basis of the module
system in the revised Definition of Standard ML 1997 [23], and
Harper and Stone [13] have formalized the elaboration of Standard
ML 1997 programs into a translucent sums calculus. To deal
with the avoidance problem, Harper and Stone rely on elaborator
mechanisms similar to ours. The Harper and Stone language can be
viewed as a subsystem of ours in which all functors are generative
and only strong sealing is supported.
Leroy introduced the notion of an applicative functor [15], which
enables one to give fully transparent signatures for many higher-order
functors. Leroy's formalism may be seen as defining purity
by a syntactic restriction that functor applications appearing in type
paths must be in named form. On one hand, this restriction provides
a weak form of structure sharing in the sense that the abstract type
F(X).t can only be the result of applying F to the module named X.
On the other hand, the restriction prevents the system from capturing
the full equational theory of higher-order functors, since not all
equations can be expressed in named form [4]. Together, manifest
types and applicative functors form the basis of the module system
of Objective Caml [27]. The manifest type formalism, like the
translucent sum formalism, does not address the avoidance prob-
lem, and consequently it lacks principal signatures.
More recently, Russo, in his thesis [28], formalized two separate
module languages: one being a close model of the SML module
system, the other being a higher-order module system with applicative
functors along the lines of O'Caml, but abandoning the named
form restriction as we do. Russo's two languages can be viewed as
subsystems of ours, the first supporting only strong sealing, the second
supporting only weak sealing. We adopt his use of existential
signatures to address the avoidance problem, although Russo also
used existentials to model generativity, which we do not. Russo's
thesis also describes an extension to SML for packaging modules as
first-class values. This extension is very similar to the existential-
packaging approach discussed in the beginning of Section 5, and
therefore suffers from the limitations of the closed-scope unpacking
construct.
While Russo defined these two languages separately, he implemented
the higher-order module system as an experimental extension
to the Moscow ML compiler [26]. Combining the two languages
without distinguishing between static and dynamic effects
has an unfortunate consequence. The Moscow ML higher-order
module system places no restrictions on the body of an applicative
in particular, one can defeat the generativity of a generative
functor by eta-expanding it into an applicative one. Exploiting this
uncovers an unsoundness in the language [6], that, in retrospect, is
clear from our analysis: one cannot convert a partial into a total
functor.
Shao [31] has proposed a single type system for modules supporting
both applicative and generative functors. Roughly speaking, Shao's
system may be viewed as a subsystem of ours based exclusively on
strong sealing and dynamic effects, but supporting both P and P par
signatures. As we observed in Section 3, this means that the bodies
of applicative functors may not contain opaque substructures (such
as datatype's). Shao's system, like ours, circumvents the avoidance
problem (Section 4) by restricting functor application and projection
to pure arguments (which must be paths in his system), and
by eliminating implicit subsumption, which amounts to requiring
that let expressions be annotated, as in our system. It seems likely
that our elaboration techniques could as well be applied to Shao's
system to lift these restrictions, but at the expense of syntactic principal
signatures. Shao also observes that fully transparent functors
may be regarded as applicative; this is an instance of the general
problem of recognizing benign effects, as described in Section 2.
7 Conclusion
Type systems for first-order module systems are reasonably well
understood. In contrast, previous work on type-theoretic, higher-order
modules has left that field in a fragmented state, with various
competing designs and no clear statement of the trade-offs (if any)
between those designs. This state of the field has made it difficult
to choose one design over another, and has left the erroneous impression
of trade-offs that do not actually exist. For example, no
previous design supports both (sound) generative and applicative
functors with opaque subcomponents.
Our language seeks to unify the field by providing a practical type
system for higher-order modules that simultaneously supports the
key functionality of preceding module systems. In the process we
dispel some misconceptions, such as a trade-off between fully expressive
generative and applicative functors, thereby eliminating
some dilemmas facing language designers.
Nevertheless, there are several important issues in modular programming
that go beyond the scope of our type theory. Chief
among these are:
. Structure Sharing. The original version of Standard ML [22]
included a notion of module equivalence that was sensitive to
the dynamic, as well as static, parts of the module. Although
such a notion would violate the phase distinction, it might be
possible to formulate a variation of our system that takes account
of dynamic equivalence in some conservative fashion.
It is possible to simulate structure sharing by having the elab-
orator add an abstract type to each structure to serve as the
"compile-time name" of that structure. However, this would
be merely an elaboration convention, not an intrinsic account
of structure sharing within type theory.
. Recursive Modules. An important direction for future re-search
is to integrate recursive modules [8, 5, 30] into the
present framework. The chief difficulty is to achieve practical
type checking in the presence of general recursively dependent
signatures, or to isolate a practical sub-language that
avoids these problems.



--R

Type Systems for Modular Programs and Specifications.
The Modula-3 type system
Abstract types and the dot notation.
Sound and complete elimination of singleton kinds.
What is a recursive module?
Moscow ML's higher-order modules are un- sound
A type system for higher-order modules (expanded version)
Cool modules for HOT languages.
Bounded existentials and minimal typing.
The undecidability of the second-order unification problem



Manifest types
Applicative functors and fully transparent higher-order modules
A syntactic theory of type generativity and sharing.
A modular module system.
Translucent Sums: A Foundation for Higher-Order Module Systems
Abstraction and Specification in Program Development.
Using dependent types to express modular structure.
A semantics for higher-order functors
The Definition of Standard ML.
David Mac- Queen
An extension of Standard ML modules with subtyping and inheritance.
Abstract types have existential type.


Types for Modules.

Recursive structures for Standard ML.
Transparent modules with fully syntactic signa- tures
Singleton Kinds and Singleton Types.
Deciding type equivalence in a language with singleton kinds.
Programming in Modula-2
--TR
Abstraction and specification in program development
Abstract types have existential type
The ModulaMYAMPERSANDndash;3 type system
Higher-order modules and the phase distinction
An extension of standard ML modules with subtyping and inheritance
Manifest types, modules, and separate compilation
A type-theoretic approach to higher-order modules with sharing
Applicative functors and fully transparent higher-order modules
Bounded existentials and minimal typing
Units
What is a recursive module?
Transparent modules with fully syntatic signatures
Deciding type equivalence in a language with singleton kinds
A type-theoretic interpretation of standard ML
Recursive structures for standard ML
Using dependent types to express modular structure
The Definition of Standard ML
A Semantics for Higher-Order Functors
Sound and Complete Elimination of Singleton Kinds
First-class structures for standard ML
Singleton kinds and singleton types

--CTR
Oleg Kiselyov , Chung-chieh Shan, Lightweight Static Capabilities, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.7, p.79-104, June, 2007
Norman Ramsey , Kathleen Fisher , Paul Govereau, An expressive language of signatures, ACM SIGPLAN Notices, v.40 n.9, September 2005
Karl Crary, Sound and complete elimination of singleton kinds, ACM Transactions on Computational Logic (TOCL), v.8 n.2, p.8-es, April 2007
Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones, Associated type synonyms, ACM SIGPLAN Notices, v.40 n.9, September 2005
Dimitrios Vytiniotis , Geoffrey Washburn , Stephanie Weirich, An open and shut typecase, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.13-24, January 10-10, 2005, Long Beach, California, USA
Derek Dreyer, A type system for well-founded recursion, ACM SIGPLAN Notices, v.39 n.1, p.293-305, January 2004
Andreas Rossberg, Generativity and dynamic opacity for abstract types, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.241-252, August 27-29, 2003, Uppsala, Sweden
Derek Dreyer , Robert Harper , Manuel M. T. Chakravarty , Gabriele Keller, Modular type classes, ACM SIGPLAN Notices, v.42 n.1, January 2007
Daniel K. Lee , Karl Crary , Robert Harper, Towards a mechanized metatheory of standard ML, ACM SIGPLAN Notices, v.42 n.1, January 2007
Derek Dreyer, Recursive type generativity, ACM SIGPLAN Notices, v.40 n.9, September 2005
Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, Theoretical Computer Science, v.375 n.1-3, p.169-192, May, 2007
Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, ACM SIGPLAN Notices, v.39 n.1, p.161-172, January 2004
James J. Leifer , Gilles Peskine , Peter Sewell , Keith Wansbrough, Global abstraction-safe marshalling with hash types, ACM SIGPLAN Notices, v.38 n.9, p.87-98, September
Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones , Simon Marlow, Associated types with class, ACM SIGPLAN Notices, v.40 n.1, p.1-13, January 2005
Andreas Rossberg, The missing link: dynamic components for ML, ACM SIGPLAN Notices, v.41 n.9, September 2006

Owens , Matthew Flatt, From structures and functors to modules and units, ACM SIGPLAN Notices, v.41 n.9, September 2006
John Billings , Peter Sewell , Mark Shinwell , Rok Strnia, Type-safe distributed programming for OCaml, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA
Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
modularity;singleton types;computational effects;functors;abstract data types;type theory;generativity