A Type System With Containers
Loading...
Date
2021-10-04
Authors
Thode, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
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.
Description
Keywords
programming languages, dependent types, ownership types, containers