pith. machine review for the scientific record. sign in

arxiv: 2605.00655 · v1 · submitted 2026-05-01 · 💻 cs.PL · cs.LO

Recognition: unknown

Type Theory With Erasure

Constantine Theocharis , Edwin Brady
Authors on Pith no claims yet

Pith reviewed 2026-05-09 14:57 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords type theoryerasurephase distinctionconservativitypresheaf modelcode extractionSOGATMartin-Löf type theory
0
0 comments X

The pith

Erasure in type theory is modeled as a phase distinction proposition in contexts, yielding conservativity over MLTT in both phases and correct extraction to untyped lambda calculus.

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

The paper constructs a structural type theory with erasure by encoding the distinction between runtime-relevant and erased data as a proposition that can appear in a context. This formulation is given as a second-order generalised algebraic theory, which admits models in categories with families and extends to any Grothendieck topos containing a tiny proposition for the phases. Conservativity over Martin-Löf type theory is shown separately for the runtime phase and the erased phase. A presheaf model is built that extracts programs to untyped lambda calculus, with correctness established by gluing. The results are accompanied by an Agda formalization and a toy elaborator.

Core claim

The central claim is that type theory with erasure can be presented as a SOGAT in which erasure is a phase distinction proposition placed in contexts. This yields separate conservativity results over MLTT for each phase and supports a presheaf model whose extracted untyped lambda terms are provably correct by gluing.

What carries the argument

The phase distinction proposition, which appears in typing contexts to separate runtime and erased terms and carries the semantics of erasure within the SOGAT structure.

If this is right

  • The theory has models in families of sets and generalizes to any Grothendieck topos equipped with a tiny proposition.
  • Code extraction proceeds via a presheaf construction that is proved correct by gluing.
  • The formulation remains compatible with additional structural features such as staging.
  • Implementation guidelines follow directly from the categorical semantics.

Where Pith is reading between the lines

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

  • This phase-based view may simplify the design of erasure passes in existing proof assistants by clarifying when data can be dropped.
  • The same mechanism could be reused for other distinctions, such as compile-time versus runtime staging or security levels.
  • The Agda formalization provides a starting point for building verified elaborators that enforce the phase distinction.

Load-bearing premise

That the phase distinction proposition integrates into the SOGAT framework while preserving its structural properties and that Grothendieck toposes with a tiny proposition model the runtime and erasure phases correctly.

What would settle it

A concrete term that is well-typed under the phase distinction but whose extracted untyped lambda calculus program fails to match the original computation, or a counter-model in which conservativity over MLTT fails in one phase.

read the original 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\"of 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.

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 / 3 minor

Summary. The paper formulates type theory with erasure as a second-order generalised algebraic theory (SOGAT) in which a phase distinction is encoded by a proposition that may appear in contexts, distinguishing runtime-relevant from erased terms. It proves conservativity over Martin-Löf type theory (MLTT) in both phases, constructs a presheaf model (in families of sets, generalising to Grothendieck toposes with a tiny proposition) that extracts to untyped lambda calculus, and establishes correctness of the extraction via gluing. All results are formalised in Agda, and a toy elaborator is provided.

Significance. The work supplies a clean, structural semantic account of erasure that is compatible with other features such as staging and that directly informs implementation. The combination of SOGAT model theory, explicit presheaf constructions, gluing-based correctness proofs, and machine-checked Agda formalisation constitutes a substantial contribution to the metatheory of dependently typed languages with erasure.

minor comments (3)
  1. §3.2: the definition of the phase proposition as a context extension could be accompanied by an explicit inductive clause showing how it interacts with the existing SOGAT signature rules, to make the integration fully mechanical.
  2. Figure 2 (presheaf model diagram): the arrow labels for the gluing functor are not fully legible at the printed size; adding a small legend or larger font would improve readability.
  3. §5.3: the statement of the extraction correctness theorem refers to 'the standard interpretation' without a forward reference to the precise equation or lemma that defines it.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. We are pleased that the combination of the SOGAT formulation, conservativity results, presheaf model with gluing, and Agda formalization is viewed as a substantial contribution.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper formulates type theory with erasure as a SOGAT with a contextual phase proposition, proves conservativity over MLTT via standard SOGAT model theory in families of sets and Grothendieck toposes with tiny propositions, constructs a presheaf model for extraction to untyped lambda calculus with gluing-based correctness, and formalizes all results in Agda. These steps rely on external categorical semantics and machine-checked proofs rather than any self-definitional reduction, fitted inputs renamed as predictions, or load-bearing self-citations whose content reduces to the present work. The derivation chain is self-contained against independent benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 1 invented entities

The paper builds on standard type theory and SOGAT model theory, introducing the phase proposition as the key new structural element for erasure.

axioms (3)
  • domain assumption Standard axioms and rules of Martin-Löf type theory
    Conservativity is established over MLTT, relying on its standard formulation.
  • standard math Model theory and definitions of second-order generalised algebraic theories (SOGATs)
    The entire formulation is presented as a SOGAT using their established theory.
  • domain assumption Existence and properties of Grothendieck toposes equipped with a tiny proposition
    Used to generalize the set-based semantics to broader categorical models.
invented entities (1)
  • Phase distinction proposition no independent evidence
    purpose: To mark runtime relevant versus erased terms when appearing in a context
    Introduced as the central structural encoding of erasure within the SOGAT.

pith-pipeline@v0.9.0 · 5496 in / 1616 out tokens · 51315 ms · 2026-05-09T14:57:14.703167+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

46 extracted references

  1. [1]

    Two-level type theory and applications , author =. Math. Struct. Comput. Sci. , publisher =. 2023 , url =

    2023

  2. [2]

    Staged compilation with two-level type theory , author =. Proc. ACM Program. Lang. , publisher =. 2022 , url =

    2022

  3. [3]

    Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , publisher =

    Type theory in type theory using quotient inductive types , author =. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , publisher =. 2016 , series =

    2016

  4. [4]

    4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) , publisher =

    Gluing for Type Theory , author =. 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) , publisher =. 2019 , url =

    2019

  5. [5]

    2024 , url =

    Second-order generalised algebraic theories: Signatures and first-order semantics , author =. 2024 , url =

    2024

  6. [6]

    Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science , publisher =

    Syntax and Semantics of Quantitative Type Theory , author =. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science , publisher =. 2018 , series =

    2018

  7. [7]

    2016 , series =

    McBride, Conor , booktitle =. 2016 , series =

    2016

  8. [8]

    Run-time Irrelevance ---

  9. [9]

    arXiv [cs.LO] , year =

    Categories with Families: Unityped, Simply Typed, and Dependently Typed , author =. arXiv [cs.LO] , year =

  10. [10]

    2021 , url =

    Abstract and concrete type theories , author =. 2021 , url =

    2021

  11. [11]

    Semantics and Logics of Computation , publisher =

    Syntax and semantics of dependent types , author =. Semantics and Logics of Computation , publisher =. 1997 , url =

    1997

  12. [12]

    Generalised algebraic theories and contextual categories , author =. Ann. Pure Appl. Logic , publisher =. 1986 , url =

    1986

  13. [13]

    Logical relations as types: Proof-relevant parametricity for program modules , author =. J. ACM , publisher =. 2021 , url =

    2021

  14. [14]

    Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90 , publisher =

    Higher-order modules and the phase distinction , author =. Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90 , publisher =. 1990 , url =

    1990

  15. [15]

    1997 , note =

    Lifting Grothendieck Universes , author =. 1997 , note =

    1997

  16. [16]

    2023 , url =

    For the metatheory of type theory, internal sconing is enough , author =. 2023 , url =

    2023

  17. [17]

    2022 , url =

    First steps in synthetic Tait computability: The objective metatheory of cubical type theory , author =. 2022 , url =

    2022

  18. [18]

    2020 , url =

    Erasure in dependently typed programming , author =. 2020 , url =

    2020

  19. [19]

    Types for Proofs and Programs , publisher =

    Inductive Families Need Not Store Their Indices , author =. Types for Proofs and Programs , publisher =. 2004 , url =

    2004

  20. [20]

    2013 , url =

    Phase Your Erasure , author =. 2013 , url =

    2013

  21. [21]

    Dependent ghosts have a reflection for free , author =. Proc. ACM Program. Lang. , publisher =. 2024 , url =

    2024

  22. [22]

    A ghost sort for proof-relevant yet erased data in Rocq and

    Winterhalter, Théo and Rosain, Johann and Sozeau, Matthieu , journal =. A ghost sort for proof-relevant yet erased data in Rocq and. 2025 , url =

    2025

  23. [23]

    2023 , url =

    Type-theoretic signatures for algebraic theories and inductive types , author =. 2023 , url =

    2023

  24. [24]

    Hugunin, Jasper , journal =. Why Not. 2021 , url =

    2021

  25. [25]

    arXiv [math.CT] , year =

    Strict universes for Grothendieck topoi , author =. arXiv [math.CT] , year =

  26. [26]

    2005 , url =

    Streicher, Thomas , booktitle =. 2005 , url =

    2005

  27. [27]

    arXiv [cs.LO] , year =

    Transpension: The right adjoint to the pi-type , author =. arXiv [cs.LO] , year =

  28. [28]

    3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) , publisher =

    Internal universes in models of homotopy type theory , author =. 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) , publisher =. 2018 , url =

    2018

  29. [29]

    arXiv [math.CT] , year =

    A Type Theory with a Tiny Object , author =. arXiv [math.CT] , year =

  30. [30]

    2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , publisher =

    Normalization for cubical type theory , author =. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , publisher =. 2021 , url =

    2021

  31. [31]

    arXiv [cs.LO] , year =

    Algebraic Type Theory and universe hierarchies , author =. arXiv [cs.LO] , year =

  32. [32]

    Compiling Programs with Erased Univalence , author =

  33. [33]

    2025 , language =

    Relative induction principles for second-order generalized algebraic theories , author =. 2025 , language =

    2025

  34. [34]

    On the relationship between

    Sterling, Jon , year =. On the relationship between

  35. [35]

    Higher-order dynamic pattern unification for dependent types and records , author =. Lect. Notes Comput. Sci. , publisher =. 2011 , url =

    2011

  36. [36]

    idris-lang/

    Dunham, Steve , year =. idris-lang/

  37. [37]

    Foundations of Software Science and Computation Structures , publisher =

    Quotient Inductive-Inductive Types , author =. Foundations of Software Science and Computation Structures , publisher =. 2018 , url =

    2018

  38. [38]

    2021 , url =

    agda/agda: Should erasure violations be hard errors more often? \# 5703 , author =. 2021 , url =

    2021

  39. [39]

    Favier, Naïm Camille , url =

  40. [40]

    Logical properties of a modality for erasure , author =

  41. [41]

    Proceedings of the 18th ACM SIGPLAN international conference on Functional programming , publisher =

    Type-theory in color , author =. Proceedings of the 18th ACM SIGPLAN international conference on Functional programming , publisher =. 2013 , url =

    2013

  42. [42]

    Foundations of Software Science and Computational Structures , publisher =

    Erasure and Polymorphism in Pure Type Systems , author =. Foundations of Software Science and Computational Structures , publisher =. 2008 , url =

    2008

  43. [43]

    arXiv [cs.PL] , year =

    Abstraction Functions as Types , author =. arXiv [cs.PL] , year =

  44. [44]

    04-implicit-args at master ·

    Kovács, András , url =. 04-implicit-args at master ·

  45. [45]

    1988 , note =

    Phase Distinctions in Type Theory , author =. 1988 , note =

    1988

  46. [46]

    1963 , url =

    Functorial semantics of algebraic theories , author =. 1963 , url =

    1963