A Type-Theoretic Approach to Higher-Order Modules with Sharing
Abstract
The design of a module system for constructing and maintaining large programs is a difficult task that at 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 oil Girard's system F omega. The calculus differs from those considered in previous studies by relying exclusively oil 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. Type theory, Modularity, Abstraction, Sharing, Functional programming, Lambda calculus.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1993
- Accession Number
- ADA273566
Entities
People
- Mark Lillibridge
- Robert Harper
Organizations
- Carnegie Mellon University