Type Theory based on Dependent Inductive and Coinductive Types

TL;DR

This paper introduces a minimalistic dependent type theory built solely on inductive and coinductive types, supporting a wide range of logical constructs and ensuring computational soundness through proven properties.

Contribution

It presents a new dependent type theory with a small rule set, capable of defining key logical and data types, and proves fundamental properties like subject reduction and strong normalization.

Findings

The type theory can define propositional connectives and data types like natural numbers.

It maintains the duality between inductive and coinductive types via categorical logic.

The reduction relation is proven to be strongly normalizing, ensuring computational consistency.

Abstract

We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theory with a small set of rules, while still being fairly expressive. For example, all well-known basic types and type formers that are needed for using this type theory as a logic are definable: propositional connectives, like falsity, conjunction, disjunction, and function space, dependent function space, existential quantification, equality, natural numbers, vectors etc. The reduction relation on terms consists solely of a rule for recursion and a rule for corecursion. The reduction relations for well-known types arise from that. To further support the introduction of this new type theory, we also prove fundamental properties of its term calculus. Most importantly, we prove subject reduction and strong normalisation of the reduction relation, which gives computational meaning to the terms. The presented type theory is based on ideas from categorical logic that have been investigated before by the first author, and it extends Hagino's categorical data types to a dependently typed setting. By basing the type theory on concepts from category theory we maintain the duality between inductive and coinductive types, and it allows us to describe, for example, the function space as a coinductive type.