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.