Master Thesis Impredicative Encodings of Inductive and Coinductive Types

TL;DR

This thesis extends impredicative encodings in System F to include inductive and coinductive types with full (co)induction principles, enabling more expressive and principled data type definitions.

Contribution

It introduces a method to encode inductive and coinductive types with induction principles in impredicative type theory, extending previous work to more general types like W-types and M-types.

Findings

Created list and quotient types with induction principles

Defined W-types with induction principles

Developed coinductive stream types with bisimulation

Abstract

In the impredicative type theory of System F ({\lambda}2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the \b{eta}-rules). Unfortunately, they do not yield a (co)induction principle, because the necessary uniqueness principles are missing (the {\eta}-rules). Awodey, Frey, and Speight (2018) used an extension of {\lambda}C with sigma-types, equality-types, and functional extensionality to provide System F style inductive types with an induction principle by encoding them as a well-chosen subtype, making them initial algebras. In this thesis, we extend their results. We create a list and quotient type that have the desired induction principles. We show that we can use the technique for general inductive types by defining W-types with an induction principle. We also take the dual notion of their technique and create a coinductive stream type with the desired coinduction principle (also called bisimulation). We finish by showing that this dual approach can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.