Definitional Functoriality for Dependent (Sub)Types – Extended version
European Symposium on Programming(2023)
摘要
Dependently typed proof assistant rely crucially on definitional equality,
which relates types and terms that are automatically identified in the
underlying type theory. This paper extends type theory with definitional
functor laws, equations satisfied propositionally by a large class of
container-like type constructors F : Type→Type,
equipped with a map_F : (A → B) → F A → F B, such as lists
or trees. Promoting these equations to definitional ones strengthens the
theory, enabling slicker proofs and more automation for functorial type
constructors. This extension is used to modularly justify a structural form of
coercive subtyping, propagating subtyping through type formers in a map-like
fashion. We show that the resulting notion of coercive subtyping, thanks to the
extra definitional equations, is equivalent to a natural and implicit form of
subsumptive subtyping. The key result of decidability of type-checking in a
dependent type system with functor laws for lists has been entirely mechanized
in Coq. This is the extended version of the work with the same name published
at ESOP'24.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要