A formalisation of parametric polymorphism within and about dependent type-theory, and an application to property-based testing

This thesis revisits the well-known notion of parametric polymorphism in the light of modern developments in type-theory. Additionally, applications of parametric polymorphism are also presented. The first part of the thesis presents a theoretical investigation of the semantics of parametric polymorphism of and within type-theories with dependent types. It is shown how the meaning of polymorphic, possibly dependent, types can be reflected within type-theory itself, via a simple syntactic transformation. This self-referential property opens the door to internalise the transformation in type-theory, and we study one possible way to do so. We also examine how the translation relates to various specific features of type-theory, such as proof irrelevance and realizability. The second part is concerned an application of parametric polymorphism relevant to software engineers. We present a schema to reduce polymorphic properties to equivalent monomorphic properties, for the purpose of testing. Our proof uses parametricity and properties of initial algebras