一句话：提出 AdapTT 类型理论，以适配器抽象刻画类型构造子的函子性，并推导归纳类型转换的结构法则。
在观察型类型论、子类型和渐进类型转换演算等依赖类型理论中，值常可在相关类型间转换（cast）。这些转换共享一种由类型构造子函子性驱动的结构行为，但此前缺乏统一而精确的刻画。本文提出并系统研究 AdapTT 类型理论，围绕类型之间抽象的 adapter（适配器）关系，将类型构造子一律做成函子式，从而统一描述 cast 的复合与保持结构。作者利用 AdapTT 中函子归纳类型的描述机制，为一般归纳类型构造子上的类型转换推导出结构法则。该工作为依赖类型中的 cast 提供了模块化、可组合的理论框架，并扩展了函子性在依赖类型论中的应用范围。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2507-13774,
title = {AdapTT: Functoriality for Dependent Type Casts},
author = {Arthur Adjedj and Meven Lennon-Bertrand and Thibaut Benjamin and Kenji Maillard},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776664}
}