A type-theoretic approach to higher-order modules with sharing

The design of a module system for constructing and maintaining large programs is a dicult task that raises a number of theoretical and practical issues. A fundamental issue is the management of the ow 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 " specications 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 F. The calculus diers 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 specication 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 sucient to encode in a straightforward way most uses o