Definitional Functoriality for Dependent (Sub)Types -- Extended version
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914745492176896 |
|---|---|
| author | Laurent, Théo Lennon-Bertrand, Meven Maillard, Kenji |
| author_facet | Laurent, Théo Lennon-Bertrand, Meven Maillard, Kenji |
| contents | 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 : \mathrm{Type} \to \mathrm{Type}$, equipped with a $\mathrm{map}_{F} : (A \to B) \to F\,A \to 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_14929 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Definitional Functoriality for Dependent (Sub)Types -- Extended version Laurent, Théo Lennon-Bertrand, Meven Maillard, Kenji Programming Languages Logic in Computer Science D.3.1; F.3.2; F.3; F.4.1 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 : \mathrm{Type} \to \mathrm{Type}$, equipped with a $\mathrm{map}_{F} : (A \to B) \to F\,A \to 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. |
| title | Definitional Functoriality for Dependent (Sub)Types -- Extended version |
| topic | Programming Languages Logic in Computer Science D.3.1; F.3.2; F.3; F.4.1 |
| url | https://arxiv.org/abs/2310.14929 |