Reconciling Software Extensibility with Modular Program Reasoning

Doctoral Dissertation, Department of Computer Science & Engineering, University of Washington (Ph.D. Dissertation), October 2003.
Todd Millstein
Programming languages that support the creation of reusable software components help make programs easier to create, maintain, and understand. To accrue these benefits in practice, a component must be extensible, able to be easily augmented from the outside by clients. A component must also support modular reasoning, providing an interface to clients that specifies the component's behavior and constraints for its proper usage.

Unfortunately, the goals of component extensibility and modular reasoning are inherently in conflict: the more extensible a component is, the harder it is to ensure properties of the component in isolation from its clients. Mainstream object-oriented (OO) and functional languages support modular reasoning in the form of modular static typechecking, which provides basic well-formedness guarantees about components. However, these languages lack some common forms of extensibility. For example, OO languages lack the functional ability to easily add new operations to existing abstractions, and functional languages lack OO-style subclassing. The conflict between extensibility and modular reasoning has forced previous languages that support these missing extensibility idioms to forgo modular typechecking.

In this dissertation, I show how programming languages can support both the OO and functional extensibility idioms while maintaining modular typechecking of components. I develop a modular type system for a simple but flexible calculus. I then apply this theoretical work to the design of practical extensions to mainstream OO and functional languages.