Carnegie Mellon University
Browse
Cavallo_CMU-CS-21-100.pdf (1.15 MB)

Higher Inductive Types and Internal Parametricity for Cubical Type Theory

Download (1.15 MB)
Version 2 2021-06-10, 20:59
Version 1 2021-05-07, 20:04
thesis
posted on 2021-06-10, 20:59 authored by Evan CavalloEvan Cavallo
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.

History

Date

2021-02-25

Degree Type

  • Dissertation

Department

  • Computer Science

Degree Name

  • Doctor of Philosophy (PhD)

Advisor(s)

Robert Harper

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC