PaperlayerView exact revision on arXiv

Source-linked AI summary

Erased Postulates, Identity Types and Quotients

Nils Anders Danielsson

arXiv:2609.08578v1cs.PLcs.LO

TL;DR

The paper asks whether postulates restricted to erased contexts can preserve computation, and extends that inquiry to identity types, quotients, and erased transports. It presents conditions under which these features are safe, while identifying a limitation for transports in the presence of []-cong.

  • Problem

    Postulates can make programs get stuck, raising the question of whether consistent postulates restricted to erased contexts preserve computation when identity types are supported.

    Source: §1 · p. 1

  • Method

    The paper analyzes erased postulates, identity types, quotient eliminators, and erased transports, including a restricted transport form in []-cong.

    Source: §3 · p. 4, §4 · p. 5, §5 · p. 7

  • Results

    Erased postulates are safe without erased matches or equality reflection, erased matches are safe without postulates and quotients, and the two can be combined when postulates are implementable using equality reflection.

    Source: §18 · p. 25

  • Takeaways & Limitations

    The quotient interface can identify related values through erased higher constructors while still guaranteeing correct numeral results for programs, even though terms may get stuck.

    Source: §3 · p. 4

    With []-cong, a variant of subst that takes an erased family and an ordinary identity proof is problematic.

    Source: §5 · p. 7

Abstract

from arXiv · show

This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.

1 Introduction

The introduction frames the risk that postulates can make programs get stuck, then presents erased postulates and identity types as a way to study when computation remains safe. It also introduces an erased quotient interface whose eliminator computes on equivalence-class constructors while retaining correct numeral results.

1 Introduction

  • Erased-postulate safety is extended to identity types, addressing whether consistent postulates restricted to erased contexts preserve computation.The introduction also presents erased matches, []-cong, and fording with erased identity proofs as contributions.Source: §1 · pp. 1–2
  • The paper studies erasure, identity types, quotients, erased matches, and []-cong, with results formalised in Agda.The formalisation spans Agda and graded type theory, with minor differences between the code and presentation.Source: §1 · p. 2

2 Erasure

  • Erased arguments cannot determine runtime decisions; in particular, an erased value cannot be used to compute a non-erased result.Erased definitions can be used only in erased contexts, and Erased A has a single box constructor taking an erased A.Source: §2 · pp. 2–3

3 Quotient Types

  • The quotient interface uses erased higher constructors and an eliminator that computes on equivalence-class constructors, but has no computation rules for the higher constructors.The interface includes a relation constructor identifying classes of related values and a set-truncation constructor.Source: §3 · pp. 3–4
  • Erased propositional extensionality and function extensionality support quotient effectiveness, which can help decide erased equality of equivalence classes.The decision procedure checks the relation between representatives and uses effectiveness to conclude inequality when the relation does not hold.Source: §3 · p. 4
  • The quotient interface is demonstrated with finite sets implemented as red-black trees quotiented by set equivalence.The implementation includes basic set operations and correctness proofs; quotient membership is defined using qrec and proposition-valued families.Source: §3 · pp. 4–5

4 Erased Postulates and Erased Matches

The paper proves erasure soundness for programs with erased matches and erased postulates when the postulates can be implemented using equality reflection. It also studies []-cong as a limited transport for erased identity proofs, since unrestricted transport is incompatible with erased univalence.

4 Erased Postulates and Erased Matches

  • When erased postulates can be implemented using equality reflection, compiled programs reduce to numerals and implementations substituted for the postulates are judgmentally equal to those numerals.The theorem allows erased matches without restriction, but requires postulates to be inhabited in the theory extended with equality reflection.Source: §4 · p. 6

5 Box-Cong

  • Erased identity-proof transport via subst′ is unsafe with erased univalence, which can yield provably distinct booleans that differ only in erased proofs.The paper also states that univalence is incompatible with UIP, so Theorem 11.3 does not apply in the presence of erased, postulated univalence.Source: §5 · p. 6
  • For vector conversion, substE uses []-cong to transport along an erased identity proof when the predicate itself accepts an erased argument.This provides an implementation of convV from VecL to VecD, addressing the problem that ordinary subst does not accept an erased identity proof.Source: §4 · p. 5, §5 · p. 7
  • []-cong encapsulates a limited erased match for identity types, and supports fording VecD with erased identity proofs; without it, fording does not work in a certain sense.Fording encodes indexed data types using regular data types and identity proofs.Source: §5 · p. 7
  • Without erased matches for single-constructor types or equality reflection, []-cong and its limited variant cannot be defined; with function extensionality, []-cong can be implemented.The paper also characterizes its definability through an equivalence involving identities of Erased values and through a left-exact modality.Source: §5 · p. 7
  • A variant subst″ with an erased predicate argument is also problematic in the presence of []-cong, producing booleans provably equal to true and false that differ only in erased proofs.The paper gives the same kind of counterexample using a three-erased-argument identity type and the function resurrect.Source: §5 · pp. 7–8

6 Towards Computational Book HoTT

The paper outlines a comparatively simple route to univalence and computation without cubical type theory, then uses erased identity proofs to encode vectors and recover a high-level eliminator. The vector encoding computes as expected, while compatibility with erased, postulated univalence and extension to other higher inductive types remain open.

6 Towards Computational Book HoTT

  • Univalence and computation can coexist without cubical type theory when single-constructor erased matches are absent, though univalence itself does not compute.This non-computation does not affect compiled programs of type ℕ; univalence can be used in the erased fragment under the stated condition.Source: §6 · p. 8
  • The work is a first step toward Computational Book HoTT, but safety for combining []-cong with erased, postulated univalence has not been proved.Whether the quotient technique extends to all higher inductive types supported by Book HoTT is also left for future work.Source: §6 · p. 8
  • A possible cubical extension would yield numeral computation and judgmental equality for compiled programs using erased postulates and []-cong, if the meta-theorem can be instantiated there.The result is conditional on suitable postulate implementations in a cubical theory with the specified features.Source: §6 · p. 8

7 Fording with Erased Identity Proofs

  • The VecD encoding uses regular data types and erased identity proofs to represent the indexed constructors’ length constraints.The nil and cons constructors carry erased proofs relating their indices to zero and successor indices.Source: §7 · p. 9
  • With []-cong, erased identity proofs support a high-level eliminator for VecF by casting case results across index equalities.JE performs these casts with an erased final identity-proof argument; its use requires a motive taking an erased natural-number argument.Source: §7 · p. 9
  • VecF-elim′ computes as expected on nil and cons, giving an encoding of VecD with expected computation behavior.Its nil case reduces to n, and its cons case reduces to c x xs applied to the recursive result.Source: §7 · p. 10
  • Without erased matches, VecF-elim′ cannot be implemented in certain type theories; unrestricted erased identity matches permit a variant with an erased motive.VecF-elim′ can also implement a limited []-cong variant that is unavailable in some such theories without erased matches.Source: §7 · p. 10
  • The VecF and VecL constructions suggest that some erased matches for identity types may be useful in a core language supporting surface-level VecD.The author expects similar ideas for more inductive families, but says that remains to be investigated.Source: §7 · p. 10

8 Type Theory with Identity Types, Quotients and Erasure

This section presents a formalized family of type theories with erasure and configurable rules for identity types, quotients, and related features. The choices affect compatibility with univalence and which erased transports can be supported.

8 Type Theory with Identity Types, Quotients and Erasure

  • The formalized theory offers identity types with choices for formation, J, and erased matches, alongside optional support for quotients, []-cong, equality reflection, and K.The formalization also includes Π-types, Σ-types, universes, natural numbers, and other type formers, though the discussion focuses on identity types, quotients, and Π-types.Source: §8 · pp. 10, 14
  • Erasure uses grades 0 and ω: grade 0 restricts use to erased contexts, while ω permits arbitrary use.The graded Π rules require bound variables and application arguments at grade 0 to remain in erased contexts.Source: §8 · pp. 10–11
  • The chosen identity-type formation rule follows Abel et al.; an alternative is incompatible with erased univalence when []-cong is present, though results hold with either rule.Equality reflection is optional and makes univalence inconsistent.Source: §8 · p. 12
  • Limited erased matches for J are equally expressive as the preceding rules plus []-cong.The unrestricted erased-match rule also permits variants of subst, but is incompatible with erased, postulated univalence.Source: §8 · p. 12
  • The Erased type boxes an erased argument, and its erased projection can be used only in erased contexts.Applying the erased projection to a box is judgmentally equal to the boxed argument.Source: §8 · p. 13
  • Quotient higher constructors are erased and treated as neutral without equality reflection; with equality reflection, well-typed applications reduce to refl.The formalization makes quotient types optional.Source: §8 · p. 13

9 Basic Meta-Theory

The paper establishes meta-theoretic properties for identity types and quotients, then proves soundness of erasure under stated restrictions. Its results include decidability and canonicity properties, alongside a boundary on when erased values can be recovered.

9 Basic Meta-Theory

  • Without quotients or with equality reflection, closed identity proofs reduce to refl and closed natural-number terms are numerals; consistency holds unconditionally.Identity canonicity does not generally hold with postulated higher quotient constructors unless equality reflection is allowed.Source: §9 · p. 14
  • Types and terms have weak head normal forms without equality reflection, or in empty contexts; identity proofs reduce to refl or a neutral term.The paper also establishes injectivity of identity types.Source: §9 · pp. 14–15
  • Judgemental equality of types and terms is decidable, and type-checking is decidable for a fragment excluding, for instance, β-redexes.The quotient constructor is also injective.Source: §9 · p. 15

10 Soundness of Erasure

  • Erasure extends the call-by-value translation to identity types and quotients, mapping identity proofs to a dummy and relating quotient classes to their extracted terms.The logical relation relates refl to the dummy value and a class term to an extraction related to its representative.Source: §10 · pp. 15–16
  • Under the theorem’s consistency or empty-type-match condition and its stated restrictions on quotients, equality reflection, and erased matches, a well-typed natural-number term and its extraction reduce to the same numeral.Unit types, and the empty type when erased matches are allowed for it, are resurrectable; natural numbers are not resurrectable at any level.Source: §10 · pp. 16–17

11 Soundness of Erasure in the Presence of Erased Postulates and Erased Matches

The paper extends erasure soundness to programs using erased postulates and erased matches by proving a closed-term result in an extended theory. It also characterizes when []-cong can be defined and when it cannot.

11 Soundness of Erasure in the Presence of Erased Postulates and Erased Matches

  • The theorem does not permit erased postulates and erased matches together, except for empty-type matches; removing its match restrictions can yield terms that do not reduce to numerals.The exception is specific to erased matches for the empty type.Source: §11 · p. 17
  • The proof replaces source reduction with judgemental equality in an extended theory, reducing the problem to soundness of erasure for closed terms.The extension must preserve typing, substitution, extraction, and closed-term soundness.Source: §11 · pp. 17–18
  • With a closing substitution into an extension satisfying the stated conditions, a well-typed natural-number term is judgementally equal to a numeral and its extraction reduces to that numeral.The result can cover programs using only postulated erased function extensionality, even with erased matches and quotient types.Source: §11 · p. 18

12 Box-Cong Can Sometimes, but Not Always, Be Defined

  • []-cong is computationally supported when the primitive is allowed, the mode is erased, equality reflection is allowed, or erased matches for J are allowed.The construction using J defines it through a variant of substE.Source: §12 · p. 19
  • Limited erased matches for J and []-cong have the same expressive power through type-preserving translations that do not affect extraction.With []-cong, a term former can also replace J with limited erased matches while retaining its stated rules.Source: §12 · p. 19
  • Without equality reflection or erased matches, []-cong cannot be defined in the stated setting, including for erased arguments.The theorem also rules out a particular erased []-cong variant for natural numbers.Source: §12 · p. 20
  • Function extensionality can define []-cong, but postulated erased function extensionality alone cannot define it in the restricted setting.A context containing only erased function extensionality is consistent, so the non-definability theorem applies.Source: §12 · p. 20

13 Modalities

The paper relates []-cong to modalities built from Erased and the box constructor. It gives equivalent characterizations of when []-cong can be defined, including a modality condition.

13 Modalities

  • If Erased and the box constructor form a modality, then []-cong can be defined.The text relates this to the modality property η-cong, which transports equalities through the unit map.Source: §13 · pp. 20–21
  • A modality consists of a type operator, a unit map, and properties including modal classification, equivalence-respect, and extendability; left exactness adds a condition on identity types.The definition allows the modality-classification type to be propositional when function extensionality holds.Source: §13 · p. 21
  • The paper defines ModalE, SeparatedE, StableE, and Stable-equalityE to describe modality and stability properties for Erased types.ModalE means that the map sending a value to its box is an equivalence; StableE gives a map from Erased A to A.Source: §13 · p. 21

14 Characterisations of “Box-Cong Can Be Defined”

  • Equivalent characterizations of []-cong include congruence for boxed values, equivalence conditions, and the availability of erased substitution or an erased J eliminator.Another characterization uses extendability along the box map.Source: §14 · pp. 21–22
  • The []-cong axiomatisation is logically equivalent to the modality structure for Erased and the box constructor.With function extensionality and propositional extensionality, the axiomatisation is a proposition.Source: §14 · p. 22

15 The Erasure Modality

The erasure modality is left exact under the stated assumption, and function extensionality suffices to establish the []-cong axiomatisation. The discussion distinguishes when erased postulates and matches are safe and identifies cubical instantiation as future work.

15 The Erasure Modality

  • The erasure modality is left exact when []-cong-axiomatisation holds, and erased equivalences induce non-erased equivalences between erased types.Erased proofs that a type is a proposition or set also show that its erased type is a proposition or set.Source: §15 · pp. 22–23
  • Some properties distinguish Erased from left exact modalities generally, including modal empty types and an erased modality property provable without []-cong.Lists of natural numbers are separated; for the closed modalities discussed, the corresponding property is tied to excluded middle.Source: §15 · pp. 22–23
  • An erasure modality property yields logical equivalences for erased function types, equivalences, equivalence maps, and H-levels.Given function extensionality, these logical equivalences can be strengthened to equivalences.Source: §15 · p. 23

16 Box-Cong Can Be Defined Using Function Extensionality

  • Function extensionality implies the []-cong axiomatisation through an equivalence for precomposition with the erasure box.The precomposition equivalence concerns functions from Erased A to Erased (P x) and their restriction along [x].Source: §16 · p. 23

17 Related Work

  • The related-work comparison distinguishes Theorem 10.1’s guarantee for every well-typed term from a prior erasure-correctness statement conditional on a term having a value [56].The paper also describes extensive prior work on erasure and notes that it is unaware of other work discussing []-cong, apart from a draft.Source: §17 · p. 24

18 Discussion

  • Erased postulates are safe with identity types under the stated conditions, while erased matches are safe without postulates and quotients.Erased matches and postulates can be combined when the postulates can be implemented in an extension with equality reflection.Source: §18 · p. 25
  • Instantiating the framework with cubical type theories to study Computational Book HoTT in the presence of []-cong is left for future work.The discussion also reports that []-cong cannot be defined without erased matches or equality reflection and relates it to limited erased matches for J.Source: §18 · p. 26

A Full Typing and Reduction Rules

The appendix presents typing and reduction rules aligned with the formalisation, with some omissions and a specialization to the erasure semiring. It also records notation and optional rule choices.

A Full Typing and Reduction Rules

  • The appendix rules match the formalisation, except for omitted optional universe levels and top-level definitions, among other smaller differences.The rules are specialized to the erasure semiring; well-scoped syntax details are omitted and should be understood as implicit.Source: A Full Typing and Reduction Rules · p. 29
  • The formalism is parametrised, allowing choices such as whether []-cong is permitted, while some rules cannot be disallowed in mode 0.The text expresses optionality through conditions on whether rules such as emptyrec are allowed in a given mode.Source: A Full Typing and Reduction Rules · p. 29
  • The appendix defines weakening and substitution notation, and universe level literals are natural numbers.The notation specifies substitution for variables 0 and 1 and weakening by a stated number of steps.Source: A Full Typing and Reduction Rules · p. 29

A.1 Typing

The typing appendix gives rules for the formal system’s data types and operations, including restrictions on erased components and configurable identity, quotient, and equality-reflection rules.

A.1 Typing

  • The appendix includes rules for reflexivity, symmetry, and transitivity, lift types, natural numbers, the empty type, and unit types.For the empty and unit types, the text specifies when their eliminators count as erased matches.Source: §A.1 · pp. 29, 30, 32
  • Erased first components of graded Σ-types can be accessed only in erased contexts, and the rules specify when product elimination counts as an erased match.The appendix also encodes Erased using unit types and graded Σ-types, with a parameter controlling whether η-equality is allowed.Source: §A.1 · pp. 31–32
  • The identity-type rules allow choices among typing rules for Id and among three rule sets for J and K.The appendix separately states typing and conversion rules for identity types and their eliminators.Source: §A.1 · pp. 32–33
  • The []-cong rule is optional, and equality reflection is separately allowed by a configurable rule.The []-cong rule produces an identity between erased values from an identity between their underlying values.Source: §A.1 · p. 34
  • Quotient rules define A/B and its class constructor, with qrec requiring a respectful method and specified coherence proofs.The appendix also gives rules for the quotient’s set condition and qrec’s typing and conversion.Source: §A.1 · pp. 34–35

A.2 Substitutions

The substitutions appendix notes that substitution definitions are omitted, gives a well-formedness relation, and defines head and tail for substitutions from non-empty contexts.

A.2 Substitutions

  • The definitions of parallel substitutions and their application to terms are omitted, but a relation for well-formed substitutions is provided.Source: §A.2 · p. 35
  • For a substitution from a non-empty context, head denotes its last term and tail denotes the remaining substitution.Source: §A.2 · p. 35

A.3 Reduction

This section specifies single-step and multi-step reduction relations for terms and types, including variants that permit evaluation under successor constructors. It also lists reduction rules involving identity types, equality reflection, and quotient terms.

A.3 Reduction

  • The displayed rules include identity-type cases for J and K, and the text explicitly allows equality reflection in the listed contexts.The equality-reflection cases include judgments involving both A/B and identity types over A/B.Source: §A.3 · pp. 35–37
  • A displayed quotient-related rule gives a reduction step for a term of A/B under premises involving the quotient type and its relation-respecting data.The rule’s conclusion is a step from w1 to w2 at type A/B.Source: §A.3 · p. 37
  • The section defines single-step and multi-step reduction relations for terms and types, with additional relations allowing evaluation under successor constructors.The β-rules for J and []-cong have judgemental-equality assumptions.Source: §A.3 · pp. 35, 37

B The Target Language

The target language is a small term language with specified values and reduction rules. The section also defines a call-by-value extraction function from source terms into that language.

B The Target Language

  • The target-language syntax includes variables, a distinguished token, unit, functions, applications, pairs, projections, and product recursion.The formalisation uses well-scoped syntax, though the text omits those details.Source: B The Target Language · p. 38
  • The value forms include the distinguished token, unit, lambdas, pairs, zero, and successor terms.The section introduces these classifications before defining single-step reduction.Source: B The Target Language · p. 38
  • Single-step reduction uses substitution, with displayed rules for product recursion and natural-number recursion; multi-step reduction is also defined.The rules reduce product recursion on a pair and natural-number recursion on zero or a successor.Source: B The Target Language · p. 38
  • The call-by-value extraction maps identity types and refl to the distinguished token, maps J and K to their computational argument, and maps quotient classes to their representative.The call-by-name variant is in the accompanying code; the extraction also maps quotient-related resp and set terms to loop and qrec to an application.Source: B The Target Language · pp. 38–39
Loading 2609.08578v1…