المفاهيم الأساسية
This paper extends Martin-Löf Type Theory (MLTT) with definitional functor laws for type constructors like lists, trees, and dependent products, enabling slicker proofs and more automation for functorial type constructors. It also uses this functorial structure to modularly justify a structural form of coercive subtyping.
الملخص
The paper extends MLTT with definitional functor laws for type constructors like lists, trees, and dependent products. This allows type constructors to be treated as functors, with a map operation that satisfies the functor laws definitionally.
The key points are:
Type constructors like lists, trees, and dependent products are equipped with a map operation that satisfies the functor laws definitionally. This avoids the need to explicitly reason about the functor laws, enabling more automation and slicker proofs.
The definitional functor laws are used to modularly justify a structural form of coercive subtyping, where subtyping is propagated through type constructors. This is shown to be equivalent to a more implicit form of subsumptive subtyping.
A type theory called MLTTmap is developed that extends MLTT with the definitional functor laws. The metatheory of MLTTmap, including normalization, canonicity, and decidable type-checking, is mechanized in Coq for a representative fragment.
Two other type theories, MLTTcoe and MLTTsub, are introduced to study the relationship between explicit coercive subtyping and implicit subsumptive subtyping. Translations between these systems are established, leveraging the definitional functor laws.
The key technical contributions are the design of MLTTmap, the metatheoretic analysis, and the connections drawn between the different subtyping approaches.