TY - GEN
T1 - Shallow embedding of type theory is morally correct
AU - Kaposi, Ambrus
AU - Kovács, András
AU - Kraus, Nicolai
PY - 2019/10/20
Y1 - 2019/10/20
N2 - 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 up to 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.
AB - 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 up to 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.
KW - Agda
KW - canonicity
KW - parametricity
KW - set model
KW - shallow embedding
KW - standard model
KW - type theory
UR - http://www.scopus.com/inward/record.url?scp=85076095331&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-33636-3_12
DO - 10.1007/978-3-030-33636-3_12
M3 - Conference contribution
SN - 9783030336356
T3 - Lecture Notes in Computer Science
SP - 329
EP - 365
BT - Mathematics of Program Construction
A2 - Hutton, Graham
PB - Springer
T2 - 13th International Conference on Mathematics of Program Construction (MPC 2019)
Y2 - 7 October 2019 through 9 October 2019
ER -