Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AdapTT: Functoriality for Dependent Type Casts

Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard

TL;DR

AdapTT provides a unified framework for structural type casting in dependent type theory by treating type formers as functors whose action on types is mediated by adapters. By modeling types as objects in NatModDOs, AdapTT encapsulates casts semantically and syntactically, and extends to AdapTT2 with type variables to internalize inductive-type signatures. The paper develops a 2D type theory that supports signatures for general inductive types, deriving functorial adapters and fusion laws, and shows how standard examples (lists, sums, W-types, Id) arise as functorial instances. Connections to generalized categories with families and presheaf models position AdapTT within established semantic frameworks, while Agda formalization demonstrates practical alignment with implementation concerns and future tooling for coercions in proof assistants.

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.

AdapTT: Functoriality for Dependent Type Casts

TL;DR

AdapTT provides a unified framework for structural type casting in dependent type theory by treating type formers as functors whose action on types is mediated by adapters. By modeling types as objects in NatModDOs, AdapTT encapsulates casts semantically and syntactically, and extends to AdapTT2 with type variables to internalize inductive-type signatures. The paper develops a 2D type theory that supports signatures for general inductive types, deriving functorial adapters and fusion laws, and shows how standard examples (lists, sums, W-types, Id) arise as functorial instances. Connections to generalized categories with families and presheaf models position AdapTT within established semantic frameworks, while Agda formalization demonstrates practical alignment with implementation concerns and future tooling for coercions in proof assistants.

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.

Paper Structure

This paper contains 65 sections, 7 theorems, 32 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Challenges of structural type casting.
  3. Introducing AdapTT
  4. Functorial type formers with AdapTT2
  5. Contributions
  6. A Category of Types
  7. AdapTT, Syntactically
  8. Models for AdapTT
  9. Comparison with Generalized Categories with Families (gCwF)
  10. Representing type formers
  11. What do we want of type variables?
  12. Lists: type variables and transformations.
  13. Identity: transformations and terms
  14. Functions and trees: contravariance
  15. $\mathop{\mathrm{\symup{\Sigma}}}\nolimits$: dependency
  16. ...and 50 more sections

Key Result

theorem 1

AdapTT interprets soundly into any NatModDO.

Figures (12)

  • Figure 1: Casts between $$ types in observational equality, subtyping and cast calculi for gradual typing.
  • Figure 2: Judgments and rules for AdapTT (excerpt, see \ref{['sec:full-rule-adaptt']})
  • Figure 3: Basic structure of AdapTT2 (excerpt)
  • Figure 4: Term variables in AdapTT2 (equations for $\sigma \mathbin{\triangleright} t$ and $\cdot^{-}$ omitted)
  • Figure 5: Rules for telescopes (excerpt) – Note that telescopes only contain term variables
  • ...and 7 more figures

Theorems & Definitions (11)

  • definition 1: NatModDO
  • theorem 1: Interpretation of AdapTT
  • definition 2
  • proposition 1
  • theorem 2
  • definition 3: Type former in a natural model
  • definition 4: Functorial structure on a type former
  • theorem 3
  • lemma 1
  • proposition 2
  • ...and 1 more