pith. sign in

arxiv: 1907.07562 · v1 · pith:JUFDVS6Tnew · submitted 2019-07-17 · 💻 cs.LO

Shallow Embedding of Type Theory is Morally Correct

Ambrus Kaposi , Andr\'as Kov\'acs , Nicolai Kraus This is my paper

Pith reviewed 2026-05-24 20:08 UTC · model grok-4.3

classification 💻 cs.LO
keywords shallow embeddingtype theorydefinitional equalitysyntactic translationimplementation hidingcanonicityparametricity
0
0 comments X

The pith

Shallow embedding of type theory syntax into the metatheory is injective up to definitional equality.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that one can reason about the syntax of a type theory by building expressions directly from the components of its standard model in the metatheory. This shallow approach reuses the metatheory's conversion checker, avoiding the technical overhead of a deep inductive encoding. To ensure soundness, the authors model the embedding itself as a syntactic translation and prove that distinct syntactic terms remain distinct up to definitional equality. They add an implementation-hiding mechanism that blocks propositional equalities and constructions that do not arise from the object syntax. The resulting setup yields short formal proofs of canonicity and parametricity.

Core claim

Shallow embedding is injective up to definitional equality because the embedding can be modelled as a syntactic translation into the metatheory; an implementation hiding trick then prevents any propositional equality proofs or other constructions that do not come from the syntax.

What carries the argument

A syntactic translation that models the shallow embedding, together with an implementation hiding mechanism that restricts constructions to those arising from the syntax.

If this is right

  • Canonicity for Martin-Löf type theory follows from a short formalisation that reuses the metatheory's conversion checker.
  • Parametricity statements can be proved by the same shallow technique without a deep encoding of the syntax.
  • The method requires only features present in any proof assistant based on dependent type theory.
  • Reasoning about syntax becomes feasible whenever the standard model is available and definitional equalities are preserved.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same translation-plus-hiding pattern could be applied to other metatheoretic properties such as normalisation or consistency.
  • If the hiding mechanism is weaker in some assistants, additional syntactic checks may be needed to restore soundness.
  • The injectivity result suggests that shallow embeddings preserve enough structure to support canonicity arguments in richer type theories.

Load-bearing premise

The standard model of the object theory has the property that all its equalities hold definitionally and that hiding suffices to exclude non-syntactic constructions.

What would settle it

An explicit pair of distinct syntactic terms whose shallow embeddings become definitionally equal, or an explicit construction that passes the hiding check yet cannot be obtained from the syntax.

Figures

Figures reproduced from arXiv: 1907.07562 by Ambrus Kaposi, Andr\'as Kov\'acs, Nicolai Kraus.

Figure 2
Figure 2. Figure 2: The termification construction [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗
read the original abstract

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\"of type theory. Our technique only requires features which are available in all major proof assistants based on dependent type theory.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims that the shallow embedding of Martin-Löf type theory into Agda, obtained by building terms from the components of the standard model, is morally correct for metatheoretic reasoning. It proves that this embedding is injective up to definitional equality by modelling the embedding as a syntactic translation targeting the metatheory, and applies an implementation-hiding construction to block propositional equalities and inhabitants that do not arise from the object syntax. The technique is demonstrated by short Agda formalizations of canonicity and parametricity, and is claimed to require only features present in all major dependent type theory proof assistants.

Significance. If the central proofs hold, the result supplies a lightweight, reusable alternative to deep embeddings for proofs that must refer to syntax (such as canonicity or normalization), by exploiting definitional equalities already present in the metatheory. The machine-checked Agda developments for injectivity, canonicity, and parametricity constitute explicit, verifiable evidence rather than informal sketches, strengthening the practical contribution.

minor comments (2)
  1. The description of the implementation-hiding construction (mentioned in the abstract and the paragraph on the model) would benefit from an explicit statement of the Agda keywords or module structure used, so that readers can immediately replicate the technique in other assistants.
  2. The claim that the technique 'only requires features which are available in all major proof assistants' is stated without a short comparison table or footnote listing the required features (e.g., definitional equality, abstract types); adding this would make the portability argument easier to verify.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and positive evaluation of the paper. We are glad that the contribution is viewed as supplying a lightweight, reusable alternative to deep embeddings, with the machine-checked developments providing verifiable evidence.

Circularity Check

0 steps flagged

No significant circularity; formal proof is self-contained

full rationale

The paper's central result is a direct formalization inside Agda: a syntactic translation is defined to model the shallow embedding, and injectivity up to definitional equality is proved from that translation; an implementation-hiding construction is then applied to exclude non-syntactic inhabitants. These steps are carried out explicitly in the object language of the proof assistant rather than by fitting parameters, renaming known results, or relying on load-bearing self-citations whose content is presupposed. The standard model's definitional equalities are a background property of the Agda metatheory, not an equation that the paper's target theorem reduces to by construction. No quoted derivation step equates the claimed injectivity result to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on the existence of a standard model inside Agda whose equalities are definitional and on Agda's module system supporting implementation hiding; these are treated as given features of the proof assistant rather than derived.

axioms (2)
  • domain assumption The standard model of Martin-Löf type theory inside Agda makes all definitional equalities hold by construction.
    Invoked in the paragraph describing the model used for shallow embedding.
  • domain assumption Agda's module and hiding mechanisms can be used to block propositional equalities and constructions not arising from the object syntax.
    Central to the second technical step; treated as a feature of the metatheory.

pith-pipeline@v0.9.0 · 5794 in / 1452 out tokens · 18596 ms · 2026-05-24T20:08:42.434195+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages · 1 internal anchor

  1. [1]

    Proceedings of the ACM on Programming Languages 2(POPL), 23 (2017) 30 A

    Abel, A., Öhman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. Proceedings of the ACM on Programming Languages 2(POPL), 23 (2017) 30 A. Kaposi et al

    work page 2017

  2. [2]

    In: Baier, C., Dal Lago, U

    Altenkirch, T., Capriotti, P., Dijkstra, G., Kraus, N., Nordvall Forsberg, F.: Quo- tient inductive-inductive types. In: Baier, C., Dal Lago, U. (eds.) Foundations of Software Science and Computation Structures. pp. 293–310. Springer International Publishing, Cham (2018)

    work page 2018

  3. [3]

    In: Bodik, R., Majumdar, R

    Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Bodik, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 18–29. ACM (2016). https://doi.org/10.1145/2837614.2837638

    work page doi:10.1145/2837614.2837638 2016

  4. [4]

    Logical Methods in Computer Science V olume 13, Issue 4 (Oct 2017)

    Altenkirch, T., Kaposi, A.: Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science V olume 13, Issue 4 (Oct 2017). https://doi.org/10.23638/LMCS-13(4:1)2017

    work page doi:10.23638/lmcs-13(4:1)2017 2017

  5. [5]

    In: A vigad, J., Mahboubi, A

    Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed template-coq. In: A vigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Lecture Notes in Computer Sc...

    work page doi:10.1007/978-3-319-94821-8_2 2018

  6. [6]

    Journal of Functional Programming 22(02), 107–152 (2012)

    Bernardy, J.P., Jansson, P., Paterson, R.: Proofs for free — parametricity for dependent types. Journal of Functional Programming 22(02), 107–152 (2012). https://doi.org/10.1017/S0956796812000056

    work page doi:10.1017/s0956796812000056 2012

  7. [7]

    In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science

    Birkedal, L., Mogelberg, R.E., Schwinghammer, J., Stovring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. pp. 55–64. IEEE (2011)

    work page 2011

  8. [8]

    In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Pro- grams and Proofs

    Boulier, S., Pédrot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Pro- grams and Proofs. pp. 182–194. CPP 2017, ACM, New York, NY, USA (2017). https://doi.org/10.1145/3018610.3018620

    work page doi:10.1145/3018610.3018620 2017

  9. [9]

    Brady, E.: Idris, a general-purpose dependently typed programming language: De- sign and implementation. J. Funct. Program. 23(5), 552–593 (2013)

    work page 2013

  10. [10]

    Electronic Notes in Theoretical Com- puter Science 228, 21–36 (Jan 2009)

    Chapman, J.: Type theory should eat itself. Electronic Notes in Theoretical Com- puter Science 228, 21–36 (Jan 2009). https://doi.org/10.1016/j.entcs.2008.12.114

    work page doi:10.1016/j.entcs.2008.12.114 2009

  11. [11]

    In: Proceedings of the 13th ACM SIGPLAN International Conference on Func- tional Programming

    Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceedings of the 13th ACM SIGPLAN International Conference on Func- tional Programming. pp. 143–156. ICFP ’08, ACM, New York, NY, USA (2008). https://doi.org/10.1145/1411204.1411226

    work page doi:10.1145/1411204.1411226 2008

  12. [12]

    TYPES 2016 (2016)

    Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. TYPES 2016 (2016)

    work page 2016

  13. [13]

    Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a construc- tive interpretation of the univalence axiom (December 2015)

    work page 2015

  14. [14]

    Canonicity and normalisation for Dependent Type Theory

    Coquand, T.: Canonicity and normalisation for dependent type theory. CoRR (2018), http://arxiv.org/abs/1810.09367

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  15. [15]

    In: Geuvers, H

    Coquand, T., Huber, S., Sattler, C.: Homotopy canonicity for cubical type theory. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) (2019)

    work page 2019

  16. [16]

    In: Altenkirch, T., McBride, C

    Danielsson, N.A.: A formalisation of a dependently typed language as an inductive- recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES. Lecture Notes in Computer Science, vol. 4502, pp. 93–109. Springer (2006)

    work page 2006

  17. [17]

    Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-Order Abstract Syntax in Coq. Tech. Rep. RR-2556, INRIA (May 1995), https://hal.inria.fr/inria-00074124 Shallow Embedding of Type Theory is Morally Correct 31

    work page 1995

  18. [18]

    In: Pro- ceedings of the 2013 ACM SIGPLAN International Conference on Func- tional Programming (ICFP 2013)

    Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Pro- ceedings of the 2013 ACM SIGPLAN International Conference on Func- tional Programming (ICFP 2013). pp. 73–85. ACM (September 2013). https://doi.org/10.1145/2500365.2500575

    work page doi:10.1145/2500365.2500575 2013

  19. [19]

    Diehl, L.: Fully Generic Programming over Closed Universes of Inductive-Recursive Types. Ph.D. thesis, Portland State University (2017)

    work page 2017

  20. [20]

    In: International Workshop on Types for Proofs and Programs

    Dybjer, P.: Internal type theory. In: International Workshop on Types for Proofs and Programs. pp. 120–134. Springer (1995)

    work page 1995

  21. [21]

    Thesis, University of Edinburgh, Department of Computer Science (1995)

    Hofmann, M.: Extensional concepts in intensional type theory. Thesis, University of Edinburgh, Department of Computer Science (1995)

    work page 1995

  22. [22]

    In: Semantics and Logics of Computation

    Hofmann, M.: Syntax and semantics of dependent types. In: Semantics and Logics of Computation. pp. 79–130. Cambridge University Press (1997)

    work page 1997

  23. [23]

    In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science

    Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science. pp. 204–. LICS ’99, IEEE Computer Society, Washington, DC, USA (1999), http://dl.acm. org/citation.cfm?id=788021.788940

    work page arXiv 1999

  24. [24]

    In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Com- puter Science

    Hou (Favonia), K.B., Finster, E., Licata, D.R., Lumsdaine, P.L.: A mecha- nization of the blakers-massey connectivity theorem in homotopy type theory. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Com- puter Science. pp. 565–574. LICS ’16, ACM, New York, NY, USA (2016). https://doi.org/10.1145/2933575.2934545

    work page doi:10.1145/2933575.2934545 2016

  25. [25]

    Huber, S.: Cubical Interpretations of Type Theory. Ph.D. thesis, University of Gothenburg (2016)

    work page 2016

  26. [26]

    In: Logics in Computer Science

    Jaber, G., Lewertowski, G., Pédrot, P.M., Sozeau, M., Tabareau, N.: The Defi- nitional Side of the Forcing. In: Logics in Computer Science. New York, United States (May 2016). https://doi.org/10.1145/2933575.2935320

    work page doi:10.1145/2933575.2935320 2016

  27. [27]

    In: Geuvers, H

    Kaposi, A., Huber, S., Sattler, C.: Gluing for type theory. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Compu- tation and Deduction (FSCD 2019) (2019)

    work page 2019

  28. [28]

    In: Kirch- ner, H

    Kaposi, A., Kovács, A.: A Syntax for Higher Inductive-Inductive Types. In: Kirch- ner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 108, pp. 20:1–20:18. Schloss Dagstuhl–Leibniz-Zentrum fuer Infor- matik, Dagstuhl, Germany (2018). https...

    work page doi:10.4230/lipics.fscd.2018.20 2018

  29. [29]

    Proceedings of the ACM on Programming Languages 3(POPL), 2 (2019)

    Kaposi, A., Kovács, A., Altenkirch, T.: Constructing quotient inductive-inductive types. Proceedings of the ACM on Programming Languages 3(POPL), 2 (2019)

    work page 2019

  30. [30]

    Kaposi, A., Kovács, A., Kraus, N.: Formalisations in Agda using a morally cor- rect shallow embedding (May 2019), https://bitbucket.org/akaposi/shallow/src/ master/

    work page 2019

  31. [31]

    Licata, D.: Running circles around (in) your proof assistant; or, quo- tients that compute (2011), http://homotopytypetheory.org/2011/04/23/ running-circles-around-in-your-proof-assistant/

    work page 2011

  32. [32]

    In: Rose, H., Shepherdson, J

    Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Rose, H., Shepherdson, J. (eds.) Logic Colloquium ’73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics, vol. 80, pp. 73–118. North- Holland (1975)

    work page 1975

  33. [33]

    LogiCal Project (2019), http://coq.inria.fr, version 8.9

    The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2019), http://coq.inria.fr, version 8.9

    work page 2019

  34. [34]

    McBride, C.: Outrageous but meaningful coincidences: dependent type-safe syn- tax and evaluation. In: d. S. Oliveira, B.C., Zalewski, M. (eds.) Proceedings of 32 A. Kaposi et al. the ACM SIGPLAN Workshop on Generic Programming. pp. 1–12. ACM (2010). https://doi.org/10.1145/1863495.1863497

    work page doi:10.1145/1863495.1863497 2010

  35. [35]

    In: Proceedings of the 2004 ACM SIGPLAN Work- shop on Haskell

    McBride, C., McKinna, J.: Functional pearl: I am not a number — I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Work- shop on Haskell. pp. 1–9. Haskell ’04, ACM, New York, NY, USA (2004). https://doi.org/10.1145/1017472.1017477, http://doi.acm.org/10.1145/ 1017472.1017477

    work page doi:10.1145/1017472.1017477 2004

  36. [36]

    In: International Conference on Automated Deduction

    de Moura, L., Kong, S., A vigad, J., Van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: International Conference on Automated Deduction. pp. 378–388. Springer (2015)

    work page 2015

  37. [37]

    Nordvall Forsberg, F.: Inductive-inductive definitions. Ph.D. thesis, Swansea Uni- versity (2013)

    work page 2013

  38. [38]

    In: Talbot, J.M., Regnier, L

    Orton, I., Pitts, A.M.: Axioms for Modelling Cubical Type Theory in a Topos. In: Talbot, J.M., Regnier, L. (eds.) 25th EACSL Annual Conference on Com- puter Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, pp. 24:1–24:19. Schloss Dagstuhl–Leibniz-Zentrum fuer Infor- matik, Dagstuhl, Germany (2016). https://doi....

    work page doi:10.4230/lipics.csl.2016.24 2016

  39. [39]

    SIGPLAN Not

    Pfenning, F., Elliott, C.: Higher-order abstract syntax. SIGPLAN Not. 23(7), 199– 208 (Jun 1988). https://doi.org/10.1145/960116.54010

    work page doi:10.1145/960116.54010 1988

  40. [40]

    In: Proceedings of the 5th Interna- tional Conference on Automated Reasoning

    Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Proceedings of the 5th Interna- tional Conference on Automated Reasoning. pp. 15–21. IJCAR’10, Springer-Verlag, Berlin, Heidelberg (2010)

    work page 2010

  41. [41]

    In: Mason, R.E.A

    Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 83, Proceedings of the IFIP 9th World Com- puter Congress, Paris, September 19-23, 1983. pp. 513–523. Elsevier Science Pub- lishers B. V. (North-Holland), Amsterdam (1983)

    work page 1983

  42. [42]

    Proceedings of the ACM on Programming Languages pp

    Tabareau, N., Tanter, É., Sozeau, M.: Equivalences for Free. Proceedings of the ACM on Programming Languages pp. 1–29 (Sep 2018), https://hal.inria.fr/ hal-01559073

    work page 2018

  43. [43]

    The Agda development team: Agda (2015), http://wiki.portal.chalmers.se/agda

    work page 2015

  44. [44]

    In: Proceedings of the 7th ACM SIGPLAN Inter- national Conference on Certified Programs and Proofs

    Wieczorek, P., Biernacki, D.: A Coq formalization of normalization by evaluation for Martin-Löf type theory. In: Proceedings of the 7th ACM SIGPLAN Inter- national Conference on Certified Programs and Proofs. pp. 266–279. CPP 2018, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3167091

    work page doi:10.1145/3167091 2018

  45. [45]

    ] = app J A BK[1] lam= t= : lam t = lam (app JtK[(1; : : :) ▷1 A=]) = lam (app JtK[ϵ; (v1; v0)][1

    Winterhalter, T., Sozeau, M., Tabareau, N.: Eliminating reflection from type the- ory. In: Proceedings of the 8th ACM SIGPLAN International Conference on Cer- tified Programs and Proofs. pp. 91–103. ACM (2019) A The injectivity displayed model We list the components of the displayed model for the injectivity proof described in Section 5. We don’t write su...

    work page 2019