The design of a module system for constructing and maintaining large
programs is a difficult task that raises a number of theoretical and
practical issues.  A fundamental issue is the management of the flow of
information between program units at compile time via the notion of an
interface.  Experience has shown that fully opaque interfaces are
awkward to use in practice since too much information is hidden, and
that fully transparent interfaces lead to excessive interdependencies,
creating problems for maintenance and separate compilation.  The
"sharing" specifications of Standard ML address this issue by allowing
the programmer to specify equational relationships between types in
separate modules, but are not expressive enough to allow the programmer
complete control over the propagation of type information between
modules.

These problems are addressed from a type-theoretic viewpoint by
considering a calculus based on Girard's system ${\sf F}_\omega$.  The
calculus differs from those considered in previous studies by relying
exclusively on a new form of weak sum type to propagate information at
compile-time, in contrast to approaches based on strong sums which rely
on substitution.  The new form of sum type allows for the specification
of equational, as well as type and kind, information in interfaces.
This provides complete control over the propagation of compile-time
information between program units and is sufficient to encode in a
straightforward way most uses of type sharing specifications in Standard
ML.  Modules are treated as "first-class" citizens, and therefore the
system supports higher-order modules and some object-oriented
programming idioms; the language may be easily restricted to
"second-class" modules found in ML-like languages.