Computer Science Department
School of Computer Science, Carnegie Mellon University
Previous higher-order module systems can be classified as either "opaque" or "transparent". Opaque systems totally obscure information about the identity of type components of modules, often resulting in overly abstract types. This loss of type identities precludes most interesting uses of higher-order features. Transparent systems, on the other hand, completely reveal type identities by inspecting module implementations, which subverts data abstraction and prevents separate compilation.
In this dissertation, I describe a novel approach that avoids these problems based on a new type-theoretic concept, the translucent sum. A translucent sum is a kind of weak sum whose type can optionally specify the identity of its type components. Under my approach type identities are not determined by inspecting module implementations, permitting separate compilation. By default, module operations reveal the connections between the types in their input and output modules. However, these connections can be obscured using type coercion. This controlled visibility permits data abstraction where desired without limiting the uses of higher-order features. My approach also allows modules to be treated as first-class values, a potentially valuable feature.
In order to lay out the groundwork for my new approach to designing higher-order module systems and to demonstrate its utility, I develop in complete detail a kernel system using my approach. I establish formally the theoretical properties of the system, including soundness even in the presence of side effects. I also show how the system may be effectively type checked.