AdapTT: Functoriality for Dependent Type Casts

TL;DR

AdapTT is a type theory that formalizes the functorial nature of type casts in dependent type systems, enabling systematic reasoning about type transformations and their structural laws.

Contribution

It introduces AdapTT, a novel type theory that captures functoriality of type formers and derives structural laws for inductive type casts.

Findings

Formalization of functorial type formers in AdapTT

Derivation of structural laws for inductive type casts

Systematic reasoning framework for type transformations

Abstract

The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.