A Type System With Containers

Abstract

In this thesis, we will introduce the concept of containers as they apply to programming languages. Encapsulation is a common topic in programming languages with well understood benefits. Here, we will investigate its converse, namely containment. This includes a demonstration of how containers can be integrated into a programming language and what benefits they can bring.

To support containment, a dependent type system is developed to enforce container rules. We add the notion of a container label to our types to indicate the container of the referred object. Around this type system we develop a language enhanced with container syntax. We use this language to show how containers can enable pass-by-value semantics, copying of complex objects and object serialization. An interpreter is implemented for this language to demonstrate its capabilities. Included is a container inferencing algorithm intended to minimize the extra syntax needed for container specification.

A second formal system is also defined. This includes type rules, operational semantics and a proof of soundness. We show that correctly-typed programs will obey all container restrictions at run-time. We fully type the configuration used by the semantics; this includes concrete containers as run-time constructs which allow us to verify correct containment. Mappings are maintained from the container labels of the language to physical run-time containers. We show that as container labels are translated across scopes (e.g. a function call), the physical containers remain consistent.

We conclude with a discussion on ways this system can be enhanced in the future to make containers easier to use, as well as describe additional capabilities such as version control of objects.