Ambrus Kaposi
Shallow Embedding of Type Theory is Morally Correct
Kaposi, Ambrus; Kov�cs, Andr�s; Kraus, Nicolai
Abstract
© 2019, Springer Nature Switzerland AG. There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to refer to the syntax, for example in proofs of canonicity and normalisation. One option is to embed the syntax deeply, by using inductive definitions in a proof assistant. However, in this case the handling of definitional equalities becomes technically challenging. Alternatively, we can reuse conversion checking in the metatheory by shallowly embedding the object theory. In this paper, we consider the standard model of a type theoretic object theory in Agda. This model has the property that all of its equalities hold definitionally, and we can use it as a shallow embedding by building expressions from the components of this model. However, if we are to reason soundly about the syntax with this setup, we must ensure that distinguishable syntactic constructs do not become provably equal when shallowly embedded. First, we prove that shallow embedding is injective upto definitional equality, by modelling the embedding as a syntactic translation targeting the metatheory. Second, we use an implementation hiding trick to disallow illegal propositional equality proofs and constructions which do not come from the syntax. We showcase our technique with very short formalisations of canonicity and parametricity for Martin-Löf type theory. Our technique only requires features which are available in all major proof assistants based on dependent type theory.
Citation
Kaposi, A., Kovács, A., & Kraus, N. (2019). Shallow Embedding of Type Theory is Morally Correct. Lecture Notes in Artificial Intelligence, 11825 LNCS, 329-365. https://doi.org/10.1007/978-3-030-33636-3_12
Journal Article Type | Conference Paper |
---|---|
Conference Name | International Conference on Mathematics of Program Construction |
Conference Location | Porto, Portugal |
Acceptance Date | Aug 22, 2019 |
Online Publication Date | Oct 20, 2019 |
Publication Date | Oct 20, 2019 |
Deposit Date | Jul 15, 2020 |
Publicly Available Date | Mar 28, 2024 |
Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Electronic ISSN | 1611-3349 |
Publisher | Springer |
Peer Reviewed | Peer Reviewed |
Volume | 11825 LNCS |
Pages | 329-365 |
Series Title | Lecture Notes in Computer Science |
Series Number | 11825 |
DOI | https://doi.org/10.1007/978-3-030-33636-3_12 |
Public URL | https://nottingham-repository.worktribe.com/output/4373315 |
Publisher URL | https://link.springer.com/book/10.1007/978-3-030-33636-3 |
Files
Shallowembedding
(218 Kb)
PDF
You might also like
Type-theoretic approaches to ordinals
(2023)
Journal Article
A rewriting coherence theorem with applications in homotopy type theory
(2022)
Journal Article
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Conference Proceeding
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
(2019)
Presentation / Conference
Univalent higher categories via complete semi-segal types
(2017)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search