| Summary: | Intuitionistic type theory was first introduced by Martin-Lof [1984] as a foundation for constructive mathematics and also serves as a dependently typed programming language. Dependent types provide us with a framework to reason about and guide the construction of programs by specifying both their structure and properties in a manner that can be automatically verified by a type-checker.
A ubiquitous pattern that arises in the formulation of dependent type abstractions involves equipping an underlying type, which captures the general form of a program, with extra structure that captures the program’s properties. Two such type abstractions include subtypes in which a type is equipped with a predicate over its values and quotient types in which a type is equipped with equations over its values. While subtypes have found much practical use in general purpose programming, quotient types have not seen many applications outside of proof assistants. Two key obstacles to the wider adoption of quotient types include an absence of practical demonstrations of their applications to general purpose programming and the significant burden of proof-obligations that arises from their use.
In this thesis, we introduce three new applications of type theoretic concepts that involve equipping types with extra structure. Firstly, we introduce a new practical application for higher-inductive types whereby they are used to encode subtypes in a manner that grants fine-grained control over the reduction behaviour of terms. Our second key contribution is the extension of a liquid type system to include a class of quotient types for which the necessary proof-obligations are decidable by an SMT-solver. This work is accompanied by a practical demonstration in the form of Quotient Haskell, which was developed as an extension to the liquid type system of Liquid Haskell. Finally, we present a constructive theory of operads, which were first introduced by Peter May to describe composable algebraic structures in symmetric monoidal structures. Intuitively, an operad can be understood as a finite family of types equipped with a well-behaved notion of composition. We demonstrate how an internalisation of the theory of operads in homotopy type theory gives rise to a generic framework for capturing and reasoning about collections of operations.
|
|---|