Mark Lillibridge

Translucent Sums: A Foundation for Higher-Order Module Systems Degree Type: Ph.D. in Computer Science
Advisor(s): Robert Harper
Graduated: May 1997

Abstract:

The ease of understanding, maintaining, and developing a large program depends crucially on how it is divided up into modules. The possible ways a program can be divided are constrained by the available modular programming facilities ("module system") of the programming language being used. Experience with the Standard-ML module system has shown the usefulness of functions mapping modules to modules and modules with module subcomponents. For example, functions over modules permit abstract data types (ADTs) to be parameterized by other ADTs, and submodules permit modules to be organized hierarchically. Module systems with such facilities are called higher-order, by analogy with higher-order functions.

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.

Thesis Committee:
Robert Harper (Chair)
Peter Lee
John Reynolds
Luca Cardelli ( DEC SRC)

James Morris, Head, Computer Science Department
Raj Reddy Dean, School of Computer Science

Keywords:
Type theory, modularity, abstraction, sharing, functional programming, lambda calculus, Standfard ML, modules and interfaces, packages, first-class modules, abstract data types