Evan Cavallo

Higher Inductive Types and Internal Parametricity for Cubical Type Theory Degree Type: Ph.D. in Computer Science
Advisor(s): Robert Harper
Graduated: May 2021

Abstract:

Recent innovation in the design of type theories–foundational systems of mathematics with a focus on constructivity–has produced the concept of interval variable, which can be used to capture relations between objects that carry computational content. We examine two such relationships in type theory: equality, in particular quotients, and arbitrary relations as applied in parametricity interpretations.

Cubical type theory, a system using an interval-based formulation of equality, enables a permissive kind of content-carrying equality that includes in particular isomorphism. Cubical type theory provides a constructive interpretation of homotopy type theory and the Univalent Foundations, formalisms that introduced the idea of isomorphism as equality but which lack intrinsic computational meaning. The cubical approach to equality also rectifies long-standing deficiencies in the behavior of quotients in type theory. We realize a system of generalized quotients for cubical type theory originally conceived in homotopy type theory, called higher inductive types, that merges the concepts of inductive type and quotient. Such a mutual generalization is particularly essential in the contentful equality setting, but also has significant applications to ordinary mathematics.

Parametricity is, among other things, a proof technique for deriving properties of constructions performed in type theories, based on the idea that constructions preserve all relations between objects. Traditionally a meta-theoretical tool, recent work has shown that parametricity properties can be integrated into a type theory itself using an interval-based system. We develop internal parametricity on top of cubical type theory, examining the similarities and distinctions between the two applications of intervals, finding that a background of cubical equality improves the behavior of internal parametricity, and applying internal parametricity as a tool to solve difficult problems in cubical type theory. We introduce a system of cohesion modalities to express the interaction between parametric and non-parametric type theory, enabling the use of parametricity results in a non-parametric setting.

Thesis Committee:
Robert Harper (Chair)
Stephen Brookes
Karl Crary
Daniel R. Licata (Wesleyan University)
Anders Mörtberg (Stockholm University)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Dependent type theory, computational semantics, cubical type theory, internal parametricity, cohesive type theory