Document Open Access Logo

Type Theory with Erasure

Authors Constantine Theocharis , Edwin Brady

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.31.pdf
  • Filesize: 1.04 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Type theory
  • erasure
  • dependent types
  • compilation
  • synthetic phase distinction
  • higher-order abstract syntax
  • logical frameworks

Metrics

Abstract

Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it has models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, which generalises to any Grothendieck topos equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory (MLTT) in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.

Cite As Get BibTex

Constantine Theocharis and Edwin Brady. Type Theory with Erasure. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.31

Author Details

Constantine Theocharis
  • University of St Andrews, United Kingdom
Edwin Brady
  • University of St Andrews, United Kingdom

Acknowledgements

We thank András Kovács, Szumi Xie, Bhakti Shah, Naïm Camille Favier and the anonymous reviewers for valuable discussions and feedback.

Supplementary Materials

References

  1. Andreas Abel, Nils Anders Danielsson, and Andrea Vezzosi. Compiling programs with erased univalence, 2022. URL: https://www.cse.chalmers.se/~ nad/publications/abel-danielsson-vezzosi-erased-univalence.pdf.
  2. Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records. Lect. Notes Comput. Sci., 6690 LNCS:10-26, 2011. URL: https://doi.org/10.1007/978-3-642-21691-6_5.
  3. Run-time irrelevance - Agda 2.9.0 documentation. URL: https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html.
  4. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Foundations of Software Science and Computation Structures, pages 293-310. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_16.
  5. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 18-29, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2837614.2837638.
  6. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. Math. Struct. Comput. Sci., 33:688-743, 2023. URL: https://doi.org/10.1017/S0960129523000130.
  7. Robert Atkey. Syntax and semantics of quantitative type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 56-65, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209189.
  8. Rafaël Bocquet. Relative induction principles for second-order generalized algebraic theories. PhD thesis, Eötvös Loránd University, 2025. URL: https://rafaelbocquet.gitlab.io/pdfs/thesis.pdf.
  9. Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the metatheory of type theory, internal sconing is enough, 2023. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.18.
  10. Edwin Brady, Conor McBride, and James McKinna. Inductive families need not store their indices. In Types for Proofs and Programs, pages 115-129. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-24849-1_8.
  11. L Cardelli. Phase distinctions in type theory. Unpublished manuscript, 1988. URL: http://lucacardelli.name/Papers/PhaseDistinctions.A4.pdf.
  12. John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  13. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. arXiv [cs.LO], 2019. URL: https://arxiv.org/abs/1904.00827.
  14. Jesper Cockx. agda/agda: Should erasure violations be hard errors more often? # 5703, 2021. URL: https://github.com/agda/agda/issues/5703.
  15. Nils Anders Danielsson. Logical properties of a modality for erasure. Technical report, University of Gothenburg, 2020. URL: https://www.cse.chalmers.se/~nad/publications/danielsson-erased.pdf.
  16. Steve Dunham. idris-lang/Idris2: Holes at unerased quantity produce bad code # 3367, 2024. URL: https://github.com/idris-lang/Idris2/issues/3367.
  17. Naïm Camille Favier. ErasureOpen. URL: https://agda.monade.li/ErasureOpen.
  18. Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for grothendieck topoi. arXiv [math.CT], 2022. URL: https://share.google/2bfRTY63iMIET0oJg.
  19. Harrison Grodin, Runming Li, and Robert Harper. Abstraction functions as types. arXiv [cs.PL], 2025. URL: https://doi.org/10.48550/arXiv.2502.20496.
  20. Adam Gundry and Conor Mcbride. Phase your erasure, 2013. URL: https://personal.cis.strath.ac.uk/conor.mcbride/pub/phtt.pdf.
  21. Robert Harper, John C Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90, pages 341-354, New York, New York, USA, 1990. ACM Press. URL: https://doi.org/10.1145/96709.96744.
  22. Martin Hofmann. Syntax and semantics of dependent types, pages 79-130. Cambridge University Press, Cambridge, 1997. URL: https://doi.org/10.1017/CBO9780511526619.004.
  23. Martin Hofmann and Thomas Streicher. Lifting grothendieck universes. Unpublished note, 1997. Google Scholar
  24. Jasper Hugunin. Why not W?, 2021. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.8.
  25. Multiplicities - Idris2 0.0 documentation. URL: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html#multiplicities.
  26. Bernardy Jean-Philippe and Guilhem Moulin. Type-theory in color. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, New York, NY, USA, 2013. ACM. URL: https://doi.org/10.1145/2500365.2500577.
  27. Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for type theory, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.25.
  28. Ambrus Kaposi and Szumi Xie. Second-order generalised algebraic theories: Signatures and first-order semantics, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.10.
  29. András Kovács. 04-implicit-args at master · AndrasKovacs/elaboration-zoo. URL: https://github.com/AndrasKovacs/elaboration-zoo/tree/master/04-implicit-args.
  30. András Kovács. Staged compilation with two-level type theory. Proc. ACM Program. Lang., 6:540-569, 2022. URL: https://doi.org/10.1145/3547641.
  31. András Kovács. Type-theoretic signatures for algebraic theories and inductive types. PhD thesis, Eötvös Loránd University, 2023. URL: https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf.
  32. F William Lawvere. Functorial semantics of algebraic theories. PhD thesis, Columbia University, 1963. URL: http://www.tac.mta.ca/tac/reprints/articles/5/tr5.pdf.
  33. Daniel R Licata, Ian Orton, Andrew M Pitts, and Bas Spitters. Internal universes in models of homotopy type theory, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  34. Conor McBride. I Got Plenty o’ Nuttin’, pages 207-233. Lecture notes in computer science. Springer International Publishing, Cham, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  35. Nathan Mishra-Linger and Tim Sheard. Erasure and Polymorphism in Pure Type Systems, pages 350-364. Springer Berlin Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_25.
  36. Andreas Nuyts and Dominique Devriese. Transpension: The right adjoint to the pi-type. arXiv [cs.LO], 2020. URL: https://doi.org/10.48550/arXiv.2008.08533.
  37. Mitchell Riley. A type theory with a tiny object. arXiv [math.CT], 2024. URL: https://doi.org/10.48550/arXiv.2403.01939.
  38. Jon Sterling. On the relationship between QTT and STC, 2023. URL: https://www.jonmsterling.com/0094/.
  39. Jonathan Sterling. Algebraic type theory and universe hierarchies. arXiv [cs.LO], 2019. URL: https://arxiv.org/abs/1902.08848.
  40. Jonathan Sterling. First steps in synthetic tait computability: The objective metatheory of cubical type theory, 2022. URL: https://doi.org/10.1184/R1/19632681.v1.
  41. Jonathan Sterling and Carlo Angiuli. Normalization for cubical type theory. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  42. Jonathan Sterling and Robert Harper. Logical relations as types: Proof-relevant parametricity for program modules. J. ACM, 68:1-47, 2021. URL: https://doi.org/10.1145/3474834.
  43. Thomas Streicher. UNIVERSES IN TOPOSES, pages 78-90. Oxford University PressOxford, 2005. URL: https://doi.org/10.1093/acprof:oso/9780198566519.003.0005.
  44. Matúš Tejiščák. Erasure in dependently typed programming, 2020. URL: https://doi.org/10.17630/STA/677.
  45. Constantine Theocharis. kontheocharis/erasure-agda. Software, (visited on 2026-07-01). URL: https://github.com/kontheocharis/erasure-agda
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26955
  46. Constantine Theocharis. kontheocharis/erasure-impl. Software, (visited on 2026-07-01). URL: https://github.com/kontheocharis/erasure-impl
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26954
  47. Taichi Uemura. Abstract and concrete type theories. PhD thesis, University of Amsterdam, 2021. URL: https://pure.uva.nl/ws/files/62028111/Thesis.pdf.
  48. Théo Winterhalter. Dependent ghosts have a reflection for free. Proc. ACM Program. Lang., 8:630-658, 2024. URL: https://doi.org/10.1145/3674647.
  49. Théo Winterhalter, Johann Rosain, and Matthieu Sozeau. A ghost sort for proof-relevant yet erased data in rocq and MetaRocq . TYPES 2025 Abstract, 2025. URL: https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper81.pdf.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact