Vortrag UNIX-Stammtisch 10/96

Vortrag UNIX-Stammtisch 10/96

In programming languages, record types give a universe of discourse (via so-called Σ-types); parameterised record types fix parts of that universe ahead of time (via Π-types), and algebraic datatypes give us first-class syntax (via W-types), which can then be used to program, e.g., evaluators and optimisers. A frequently-encountered issue in library design for statically-typed languages is that, for example, the algebraic datatype implementing the first-class view of the language induced by a record declaration cannot be defined by simple reference to the record type declaration, nor to any common “source”. This leads to unwelcome repetition, and to maintenance burdens. Similarly, the “unbundling problem” concerns similar repetition that arises for variants of record types where some fields are turned into parameters. The goal of this thesis is to show how, in dependently-typed languages (DTLs), algebraic datatypes and parameterised record types can be obtained from a single pragmatic declaration within the dependently-typed language itself, without using a separate “module language”. Besides this practical shared declaration interface, which is extensible in the language, we also find that common data structures correspond to simple theories. Put simply, the thesis is about making tedious and inexpressible patterns of programming in DTLs (dependently typed languages) become mechanical and expressible. The situations described above occur frequently when working in a dependently-typed language, and it is reasonable enough to have the computer handle them. We develop a notion of contexts that serve as common source for definitions of algebraic datatype and of parameterised record types, and demonstrate a “language” of “package operations” that enables us to avoid the above-mentioned replication that pervades current library developments. On the one hand, we demonstrate an implementation of that language as integrated editor functionality — this makes it possible to directly emulate the different solutions that are employed in current library developments, and refactor these into a shape that uses single declaration of contexts, thus avoiding the usual repetition that is otherwise required for provision of record types at different levels of parameterisation and of algebraic datatypes. On the other hand, we will demonstrate that the power of dependently-typed languages is sufficient to implement such package operations in a statically-typed manner within the language; using this approach will require adapting to the accordingly-changed library interfaces. Although our development uses the dependently-typed programming language Agda throughout, we emphasise that the idea is sufficiently generic to be implemented in other DTLs. / Thesis / Doctor of Philosophy (PhD) / There are things we want to use from various perspectives, our tools show that this is possible without any duplication and in a practical and efficient fashion.