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.
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/26373 |
| Date | January 2021 |
| Creators | Al-hassy, Musa |
| Contributors | Kahl, Wolfram, Carette, Jacques, Computing and Software |
| Source Sets | McMaster University |
| Language | English |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.002 seconds