a type-theoretic approach to higher-order modules with sharing
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 separated 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 &ohgr; . The calculus differs form 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 users 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.
types module sharing design systems program task practical management flow informal timing interfaces experience use transparency maintenance separate compilation standardization addressing programmer relationships express completeness control propagation encode users object-oriented programming language  ml  order class