AdapTT: Functoriality for Dependent Type Casts
summary
A new type theory AdapTT formalizes adapters as external morphisms that form a category and lets every type former act functorially on those adapters so casts compose and reduce predictably, with functoriality preserves identities and composition definitionally to avoid coherence bugs. A generic transformation rule applies adapter data to instantiated types, proofs yield a generalized map for inductive types that preserves composition and identities definitionally, an experimental NbE implementation exists and artifacts are available and evaluated.
AI-written summary · about
chapters (7)
- 0:00AdapTT introduction
- 2:06Coercion system problems
- 3:51Adapters as new concept
- 8:05Type formers with casts
- 13:19Two-categorical structure
- 18:14Implementation and future
- 20:19Q&A
related talks
37mTypes that Change: The Extensible Type Design Pattern
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
24mGeneralization of meta programs with dependent types in mtac2 with mtac2
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
14mProgram Adverbs and Tlon Embeddings
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
11mHigher order Abstractions
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2