Pith. sign in

REVIEW 3 major objections 5 minor 37 references

Custom Representations of Inductive Families

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proposes giving every inductive family a user-defined runtime representation, with proofs that converting between a type and its representation costs nothing at runtime.

desk verdict The core idea is new and the Agda formalization is real, but the headline zero-cost erasure guarantee rests on an unformalized extraction step. read the letter →

arxiv 2505.21225 v2 pith:N7SKS5QW submitted 2025-05-27 cs.PL

Constantine Theocharis , Edwin Brady This is my paper
classification cs.PL MSC 03B3868N18
keywords dependenttypesinductivefamiliescustomdatarepresentationsmemoryrepresentationerasurealgebrasviewscompilation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper sets out to show that programmers can attach a custom runtime representation to any inductive family — Nat as a big integer, a vector as the list it refines — and the compiler will erase the entire conversion layer, leaving no runtime traces and needing no optimization heuristics such as deforestation. This matters because dependently typed languages default to linked-tree data representations, and today's alternatives are compiler special cases like the 'Nat-hack' or real runtime costs when converting between differently indexed views of the same data. The system works by treating a representation as an inductive algebra for the type's signature and by providing a translation $R$ to extensional type theory that replaces every data type with its underlying algebra while erasing the $\mathrm{Repr}$ modality's $\mathtt{repr}$ and $\mathtt{unrepr}$, which are definitional inverses and therefore computationally irrelevant. If the paper is right, optimisations that are currently hard-coded in compilers become ordinary library definitions, and conversions such as forgetting or remembering a vector's length become identity functions at runtime.

What carries the argument

The load-bearing device is the inductive algebra, defined as a representation of a signature $S$ (Definition 2): a carrier type $X$ together with an algebra $\alpha$ that interprets the constructors of $S$ and an induction witness $\kappa$ certifying that the algebra supports elimination. The translation $R$ (Section 3.6) carries the argument: it replaces every data type $\mathtt{data}_\Delta\ S\ \gamma$ with the carrier $\gamma.X$, each constructor with the corresponding algebra operation $\gamma.\alpha_O$, and each eliminator with the section produced by $\gamma.\kappa$, and it erases $\mathtt{repr}$ and $\mathtt{unrepr}$ wherever they occur. The $\mathrm{Repr}$ modality is the intensional shadow of that translation: $\mathrm{Repr}\ A$ is not definitionally equal to $A$, yet $\mathtt{repr}$ and $\mathtt{unrepr}$ are definitional inverses, so every round-trip between a data type and its representation is computationally irrelevant once $R$ has been applied.

What would settle it

Compile the forget-length and remember-length functions of section 2.2 with the prototype implementation and inspect the generated JavaScript at each conversion site, because the paper's claim predicts that no residual conversion function, closure, or branch on the length index appears there; a surviving $\mathtt{repr}$ or $\mathtt{unrepr}$ operation would show the erasure promise stops short of the code generator. A second check is to run the postulated eliminator equations for big integers against the actual primitive implementation, since a representation target that fails its postulates cannot be repaired by erasure.

Watch

Extended reading notes

Core claim

The paper's central claim is that a represented inductive family will not leave any runtime traces behind, and that this requires no optimization heuristics such as deforestation because it is a consequence of the translation itself. The paper defines a dependent type system, datatt, in which an inductive family is a type $\mathtt{data}_\Delta\ S\ \gamma$ built from a signature $S$ and an inductive algebra $\gamma$; a representation is simply another inductive algebra for the same signature, and the system's $\mathrm{Repr}$ modality supplies term formers $\mathtt{repr}$ and $\mathtt{unrepr}$ that are definitional inverses, making the isomorphism between a type and its representation computationally irrelevant. A type- and equality-preserving translation $R$ from datatt to extensional Martin-Löf type theory replaces every data type with the carrier of its underlying algebra, every constructor with the corresponding algebra operation, and every eliminator with the induction section of that algebra; three theorems, verified in a machine-checked formalisation, state that $R$ preserves typing and equality, that $R$ is a left-inverse of the inclusion of the base theory into datatt, and that $\mathrm{Repr}$ is injective up to equivalence with computationally irrelevant conversion. Consequently the Nat-hack, the forget-length and remember-length functions between vectors and lists, and the projection functions of a zero-copy deserialisation example all compile to the identity at runtime.

Load-bearing premise

The zero-runtime-trace guarantee rests on an extraction step $|{-}|$ from the translation's target language to a runtime language that the paper describes only informally, and on primitive representation targets such as big integers actually satisfying the equations they are postulated to satisfy; if either fails, the claimed erasure does not follow.

Editorial extensions

If this is right

  • The 'Nat-hack' stops being a compiler special case: representing Nat as big unsigned integers with a coherent eliminator is library code, and after $R$ the representation is gone from the compiled program.
  • Reindexing conversions between $\mathrm{Vec}\ T\ n$ and $\mathrm{List}'\ T\ n$ — the forget-length and remember-length functions — compile to the identity function, giving zero-cost reuse of the underlying list data.
  • Representations compose transitively: if List itself gets a custom representation, Vec silently inherits it at runtime, while $\mathrm{Repr}\ (\mathrm{Vec}\ T\ n)$ still computes to $\mathrm{List}\ T$.
  • Zero-copy deserialisation becomes expressible: a Player record represented as a byte buffer plus an erased proof compiles field access down to buffer slicing, with the projection functions erasing to identity.
  • Because $R$ preserves typing and equality and is a left-inverse of the inclusion of the base theory, programmers can reason with the high-level inductive structure while execution happens entirely on the representation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A boundary the paper leaves implicit: the zero-trace guarantee is proven for the translation $R$, not for the informal extraction step that follows it, so the guarantee reaches the code generator only to the extent that the extraction actually implements the stated erasure.
  • The paper's own future-work agenda points at quotient-inductive types; if the erasure machinery extends there, data structures such as hash maps and binary search trees could be used inductively in reasoning while compiling without redundant representation.
  • A litmus test suggested by the framework: a compiler optimisation is a candidate for library-level, verified status exactly when it can be packaged as an inductive algebra with a coherent elimination, and optimisations that resist such packaging are likely the ones that stay heuristic.
  • Porting the pattern to existing dependently typed compilers would mean exposing the representation translation as a user-facing feature rather than a built-in hack, and the prototype described in the paper suggests the mechanism is small enough to fit.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces a language extension, datatt, to Martin-Löf type theory in which inductive families are defined together with an explicit inductive algebra (carrier, operations, induction principle) that serves as the data type's runtime representation. Programmers can declare representations such as Nat as UBig or Vec as a refinement of List; the language provides a Repr modality with repr/unrepr that are definitional inverses, enabling conversion between a data type and its representation. The main formal result is a translation R from datatt to extensional MLTT that replaces every data type by the carrier of its inductive algebra and every eliminator by the induction principle of the representation; Theorems 1 and 2 (type/equality preservation and left-inverseness to the inclusion of MLTT) are formalized in Agda. The paper also sketches an extraction step |−| to a runtime language, claims computational irrelevance of repr/unrepr and of refinement projections, and describes a prototype implementation in Superfluid.

Significance. The central idea is attractive and timely: giving users control over the runtime representation of inductive families while retaining dependent pattern matching and propositional coherence, with the key correctness theorems machine-checked in Agda. The paper is honest about limitations (unformalized extraction, postulated UBig equations, no coherence proofs required in the implementation). If the extraction assumptions were formalized, this would be a strong foundation for zero-cost views; as it stands the abstract's 'will not leave any runtime traces' guarantee is conditional on an unproven backend property. Strengths: the inductive-algebra semantics for representations, the Agda formalization of R, and the transitivity/refinement examples.

major comments (3)
  1. [§3.7, Definition 3 and Theorem 3] Theorem 3 formally states that convp is computationally irrelevant only assuming |−| erases internal equality reasoning, but the main claim of the abstract -- that a represented inductive family 'will not leave any runtime traces behind' -- relies on more than that. The forget-length/remember-length examples require the specific erasure postulates for subset types (|{A|B}| = |A|, |(x,y)| = |x|, |π1 x| = |x|) which are stipulated in §3.7, not derived from the formalized R or from Theorem 3. Since |−| is never formalized, the zero-cost property is an assumption about the code generator rather than a theorem.
  2. [§2.1, UBig postulates] The Nat-as-UBig example is load-bearing for the paper's motivation ('a library of convenient inductive families based on a minimal set of primitives'), but its correctness depends on two postulated equations (ubig-elim-zero-id and ubig-elim-add-one-id). The paper explicitly says these are a separate concern; that is a reasonable scope decision, but it means the headline example is not a theorem about actual GMP integers. Without evidence (even a proof sketch) that such a ubig-elim exists for the intended primitive, the example remains conditional.
  3. [§4, Implementation] The Superfluid implementation does not require the coherence proofs (eliminator coherence) that the formal system demands, and it treats the constructor-representation rule as definitional. This is a discrepancy between the prototype and the formal language. The paper acknowledges it, but for the claim that the framework 'guarantees erasure of abstraction layers' the implementation provides only partial validation because the checked property is not the one used in the compiler.
minor comments (5)
  1. [§1, Introduction] The phrase 'This is not erased by any current language with dependent types' is strong; consider qualifying it with 'to our knowledge' and citing the closest relevant mechanisms (erased indices in Agda/Idris, qtt-based irrelevance) more precisely.
  2. [§3.6, Figure 5] The notation R(i(a)) in Theorem 2 is not defined in the figure; spelling out the inclusion i would help.
  3. [§3, paragraph after Definition 1] There is a typo: 'the follwing objects' should be 'the following objects'.
  4. [§4, implementation] The examples directory and the claim that some examples are written in Superfluid would benefit from a concrete list of which examples (e.g., Nat-as-UBig, Vec-as-List') are actually runnable.
  5. [References [33],[36]] Reference [33] appears to point to an Idris2 pull request while being cited as an Agda issue; the URLs for [33] and [36] look mismatched and should be checked.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central translation and erasure theorems are proved in Agda, and the extraction-based irrelevance claim is an explicitly stated backend assumption rather than a circular reduction.

full rationale

The paper's derivation chain is self-contained rather than circular. The central theorems (Theorems 1-3, Section 3.6 and Section 3.7) state that the translation R preserves typing and definitional equality, that R is a left inverse of the inclusion of MLTT into datatt, and that Repr-based conversions become definitional identities after translation; these are proved in the accompanying Agda formalisation (Section 8), so they do not rest on a self-citation or on fitting a parameter to the result being 'predicted'. The Nat example in Section 2.1 explicitly separates the postulated UBig eliminator equations from the correctness of the representation framework itself, saying: 'We expect that the underlying implementation of UBig indeed satisfies these postulated properties, which is a separate concern from the correctness of the representation itself', and the Vec/List and general reindexing examples build the relevant eliminators and coherence proofs rather than assuming the conclusion. Section 3.7 defines computational irrelevance relative to an informally specified extraction function |−|, and Theorem 3 assumes that |−| erases equality reasoning and subset projections; this is a backend soundness assumption, making the zero-runtime-traces claim conditional on the code generator, but it is not a circular reduction of a prediction to its own input, a fitted-parameter disguise, or a load-bearing self-citation. No specific equation or theorem in the paper reduces to its own conclusion by construction.

Assumptions & free parameters 0 free parameters · 6 assumptions · 1 invented entities

The central claim depends on standard MLTT plus several simplifying assumptions (U:U, extensional equality, postulates for primitives) and an unformalized extraction step. The Agda formalisation covers the core translation theorems, which is strong evidence, but the listed axioms are not all machine-checked.

assumptions (6)
  • domain assumption U : U (single universe in the formalization)
    Section 3 states 'We omit considerations of consistency and universe hierarchy, though these can be added if needed.' This is a simplification that is potentially inconsistent in standard set-theoretic semantics, but common in type-theoretic presentations.
  • domain assumption Extensional MLTT with equality reflection as the target of R
    The translation R in section 3.6 targets extensional MLTT, which has the equality reflection rule. This is a strong extension not present in the source datatt, and it is used to turn propositional coherence into definitional equality.
  • ad hoc to paper Postulated equations for UBig: ubig-elim-zero-id and ubig-elim-add-one-id
    Section 2.1 states 'we expect that the underlying implementation of UBig indeed satisfies these postulated properties, which is a separate concern'. The Nat representation relies on these postulates.
  • domain assumption Decidability of type checking for datatt
    Section 3.6 says type checking is decidable for datatt, 'not formalised in this paper'. This is needed to justify applying the translation after type checking.
  • ad hoc to paper The extraction step |−| erases internal equality reasoning and repr and unrepr
    Section 3.7 defines computational irrelevance using |−| and Theorem 3 assumes |−| erases equality reasoning. This extraction is not formalized.
  • domain assumption Availability of W-types or primitive data types in the target to construct inductive algebras in an empty context
    Section 3.6 notes that basic MLTT is not sufficient to construct most inductive algebras in an empty context; the implementation falls back to a default data type. This is an assumption about the target's strength.
invented entities (1)
  • Repr modality independent evidence
    purpose: A type former that maps a data type to its representation, with repr and unrepr terms that are definitional inverses, enabling type-directed conversion between a data type and its representation.
    The modality is formalized in Agda, its computation rules are given in fig. 4, and the translation R erases it (section 3.6). The implementation in Superfluid supports it. It has a clear specification, so it is not an unjustified new primitive.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Custom Representations of Inductive Families." pith.science (2026). https://pith.science/paper/N7SKS5QW

@misc{pith2026250521225,
  author       = {Pith},
  title        = {Pith review of: Custom Representations of Inductive Families},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/N7SKS5QW}},
  note         = {Machine review of arXiv:2505.21225}
}
read the original abstract

Inductive families provide a convenient way of programming with dependent types. Yet, when it comes to compilation, their default linked-tree runtime representations, as well as the need to convert between different indexed views of the same data, can lead to unsatisfactory runtime performance. In this paper, we introduce a language with dependent types, and inductive families with customisable representations. Representations are a version of Wadler's views, refined to inductive families like in Epigram, but with compilation guarantees: a represented inductive family will not leave any runtime traces behind, without relying on heuristics such as deforestation. This way, we can build a library of convenient inductive families based on a minimal set of primitives, whose re-indexing and conversion functions are erased during compilation. We show how we can express optimisation techniques such as representing Nat-like types as GMP-style big integers, without special casing in the compiler. With dependent types, reasoning about data representations is also possible through a provided modality. This yields computationally irrelevant isomorphisms between the original and represented data.

Figures

Figures reproduced from arXiv: 2505.21225 by the authors.

Figure 1
Figure 1. Rules for forming telescopes and spines. Extending contexts by telescopes (such as Γ, ∆) is defined by induction on telescopes. We write ∆ → X for an iterated function type with codomain Γ, ∆ ⊢ X, and (δ :: ∆) → X[δ] when names are highlighted. We will often use the notation δ.y to extract a certain index y from a spine δ. This is used when we define telescopes using named notation. For example, if δ :: (X : A → U, … view at source ↗
Figure 2
Figure 2. Rules for forming signatures and operations. Each signature is described by an associated telescope of indices ∆, and a finite list of operations: – (x : A) →ext O[x], a (dependent) abstraction over some external type A, of another operation O. – ι δ →int O, an abstraction over a recursive occurence of the object being defined, with indices δ, of another operation O. – ι δ, a constructor of the object being defined,… view at source ↗
Figure 3
Figure 3. Rules for data types, constructors and eliminators. We write O ∈ S to indicate that O is an operation in the signature S. We write αO to extract the telescope element corresponding to operation O from the algebra α for S. principle suggests that the constructors corresponding to each method are dis￾joint. Since constructors ctor are primitive terms in the theory, we can make use of this when formulating a unificatio… view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Introduction and elimination forms, as well as computation rules for the Repr modality. These rules allow us to go between a data type D = data∆ S γ δ and its representation γ.X δ. In the translation to extensional mltt that we are yet to define, this modality is also …
Figure 5
Figure 5. Figure 5: Translation of datatt to mltt, replaces data types with their underlying induc￾tive algebras, and eliminators by the induction principle provided by representations. All the mappings above are structurally recursive, demonstrated by the con￾struction of a model of data…
Figure 6
Figure 6. Figure 6: Equality translation of datatt to extensional mltt. This amounts to an in￾ductive proof that R preserves equality. Theorem 1 (agda). R preserves typing and definitional equality [PITH_FULL_IMAGE:figures/full_fig_p018_6.png]
Figure 7
Figure 7. Figure 7: Typing rules for mltt [PITH_FULL_IMAGE:figures/full_fig_p026_7.png]
Figure 8
Figure 8. Figure 8: Definitional equality rules for mltt, omitting substitution rules such as (El a)[σ] = El (a[σ]). 8.2 Definition of datatt The language datatt is the extension of mltt. by the rules in figs. 3 and 4. Below we present some additional definitional equality rules of Repr t…
Figure 9
Figure 9. Figure 9: (agda) Definitional compatibility rules for Repr. Similar rules are given for Σ and ⊤ in the formalisation. In this version, Repr only applies to codomains of functions which aligns with the substitution rule. However, it is also possible to formulate it as Repr ((x : …
Figure 10
Figure 10. Figure 10: Additional propositional equalities for Repr on constructors and eliminators. Here, repr∗ applies Repr on all the recursive arguments of a displayed algebra. The rule elim-equivS {γ} M β δ x is also derivable internally by case analysis on x [PITH_FULL_IMAGE:figures/…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

37 extracted references · 30 canonical work pages

  1. [1]

    In: Automata, Languages and Programming, pp

    Abbott, M., Altenkirch, T., Ghani, N.: Representing nested inductive types using W-types. In: Automata, Languages and Programming, pp. 59–71. Lecture notes in computer science, Springer Berlin Heidelberg, Berlin, Heidelberg (2004),https: //link.springer.com/chapter/10.1007/978-3-540-27836-8_8

    work page doi:10.1007/978-3-540-27836-8_8 2004

  2. [2]

    thesis, https://www2.tcs.ifi.lmu.de/~abel/talkHabil2013.pdf Custom Representations of Inductive Families 23

    Abel,A.:Normalizationbyevaluation:Dependenttypesandimpredicativity.Ph.D. thesis, https://www2.tcs.ifi.lmu.de/~abel/talkHabil2013.pdf Custom Representations of Inductive Families 23

    work page

  3. [3]

    Adamek, J., Rosicky, J., Vitale, E.M.: Cambridge tracts in mathematics: Algebraic theories: A categorical introduction to general algebra series number 184. Cambridge University Press, Cambridge, England (18 Nov 2010), https://www.cambridge.org/academic/subjects/mathematics/logic- categories-and-sets/algebraic-theories-categorical-introduction- general-al...

    work page 2010

  4. [4]

    In: Programming Lan- guages and Systems

    Allais, G.: Builtin types viewed as inductive families. In: Programming Lan- guages and Systems. pp. 113–139. Springer Nature Switzerland (2023), http: //dx.doi.org/10.1007/978-3-031-30044-8_5

    work page doi:10.1007/978-3-031-30044-8_5 2023

  5. [5]

    Seamless, Correct, and Generic Programming over Serialised Data

    Allais, G.: Seamless, correct, and generic programming over serialised data. arXiv [cs.PL] (20 Oct 2023),http://arxiv.org/abs/2310.13441

    work page Pith review arXiv 2023

  6. [6]

    Frex: dependently-typed algebraic simplification

    Allais, G., Brady, E., Corbyn, N., Kammar, O., Yallop, J.: Frex: dependently- typed algebraic simplification. arXiv.org (2023), http://dx.doi.org/10.48550/ ARXIV.2306.15375

    work page Pith review arXiv doi:10.48550/arxiv.2306.15375 2023

  7. [7]

    In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

    Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 18–29. POPL ’16, Association for Computing Machinery, New York, NY, USA (11 Jan 2016), https://doi.org/ 10.1145/2837614.2837638

    arXiv 2016

  8. [8]

    In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

    Atkey, R.: Syntax and semantics of quantitative type theory. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 56–

    work page

Show all 37 references
  1. [9]

    Atkey, R., Johann, P., Ghani, N.: When is a type refinement an inductive type? In: Foundations of Software Science and Computational Structures, pp. 72–87. Lecture notes in computer science, Springer Berlin Heidelberg, Berlin, Heidelberg (2011), https://bentnib.org/inductive-r...

    2011

  2. [10]

    Baudon, T., Radanne, G., Gonnord, L.: Bit-stealing made legal: Compilation for custom memory representations of algebraic data types. Proc. ACM Program. Lang. 7(ICFP), 813–846 (31 Aug 2023),https://doi.org/10.1145/3607858

    2023 doi

  3. [11]

    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, Association for Computing Machinery, New York, NY, USA (16 Jan 2017),https://do...

    2017

  4. [12]

    In:TypesforProofsandPrograms.pp.115–129.SpringerBerlinHeidelberg(2004), http://dx.doi.org/10.1007/978-3-540-24849-1_8

    Brady,E.,McBride,C.,McKinna,J.:Inductivefamiliesneednotstoretheirindices. In:TypesforProofsandPrograms.pp.115–129.SpringerBerlinHeidelberg(2004), http://dx.doi.org/10.1007/978-3-540-24849-1_8

    2004 doi

  5. [13]

    arXiv [cs.LO] (1 Apr 2019),http://arxiv.org/ abs/1904.00827

    Castellan,S.,Clairambault,P.,Dybjer,P.:Categorieswithfamilies:Unityped,sim- ply typed, and dependently typed. arXiv [cs.LO] (1 Apr 2019),http://arxiv.org/ abs/1904.00827

    2019 arXiv

  6. [14]

    Cockx, J., Devriese, D.: Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory. J. Funct. Prog.28(e12), e12 (Jan 2018), https://www.cambridge.org/core/services/aop-cambridge-core/content/ view/E54D56DC3F5D5361CCDECA824030C38E/S09567968...

    2018

  7. [15]

    In: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science

    Dagand, P.E., McBride, C.: A categorical treatment of ornaments. In: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE (Jun 2013), http://dx.doi.org/10.5555/2591370.2591396 24 Constantine Theocharis and Edwin Brady

    2013

  8. [16]

    Diehl, L., Firsov, D., Stump, A.: Generic zero-cost reuse for dependent types. Proc. ACM Program. Lang. 2(ICFP), 1–30 (30 Jul 2018), https://doi.org/10.1145/ 3236799

    2018

  9. [17]

    In: Algebra, Meaning, and Computation, pp

    Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern match- ing. In: Algebra, Meaning, and Computation, pp. 521–540. Lecture notes in computer science, Springer Berlin Heidelberg, Berlin, Heidelberg (2006),https: //research.google.com/pubs/archive/99.pdf

    2006

  10. [18]

    In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

    Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, New York, NY, USA (8 Jul 2020),http://dx.doi.org/ 10.1145/3373718.3394736

    2020

  11. [19]

    Kovács, A.: Staged compilation with two-level type theory. Proc. ACM Pro- gram. Lang. 6(ICFP), 540–569 (29 Aug 2022),https://dl.acm.org/doi/10.1145/ 3547641

    2022

  12. [20]

    Kovács, A.: Type-theoretic signatures for algebraic theories and induc- tive types. Ph.D. thesis (2023), https://andraskovacs.github.io/pdfs/ phdthesis_compact.pdf

    2023

  13. [21]

    Martin-Löf, P.: Intuitionistic type theory 1, 1–91 (1984), https: //intuitionistic.wordpress.com/wp-content/uploads/2010/07/martin- lof-tt.pdf

    1984

  14. [22]

    In: Lecture Notes in Computer Science, pp

    McBride, C., Goguen, H., McKinna, J.: A few constructions on constructors. In: Lecture Notes in Computer Science, pp. 186–200. Lecture notes in computer science, Springer Berlin Heidelberg, Berlin, Heidelberg (2006), http://www.e- pig.org/downloads/concon.pdf

    2006

  15. [23]

    Mcbride, C., Mckinna, J.: The view from the left. J. Funct. Programming 14(1), 69–111 (Jan 2004), https://www.cambridge.org/core/services/ aop-cambridge-core/content/view/F8A44CAC27CCA178AF69DD84BC585A2D/ S0956796803004829a.pdf/div-class-title-the-view-from-the-left-div .pdf

    2004

  16. [24]

    In: Programming Languages and Systems

    Moon, B., Eades, III, H., Orchard, D.: Graded modal dependent type theory. In: Programming Languages and Systems. pp. 462–490. Springer International Pub- lishing (2021), http://dx.doi.org/10.1007/978-3-030-72019-3_17

    2021 doi

  17. [25]

    In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

    Wadler, P.: Views: a way for pattern matching to cohabit with data abstraction. In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. pp. 307–313. POPL ’87, Association for Computing Ma- chinery,New York,NY, USA(1Oct 1987), https://do...

    1987

  18. [26]

    Wadler, P.: Deforestation: transforming programs to eliminate trees. Theor. Com- put. Sci.73(2), 231–248 (1 Jun 1990),https://www.sciencedirect.com/science/ article/pii/030439759090147A

    1990

  19. [27]

    https://wiki.portal.chalmers.se/agda/pmwiki.php, accessed: 2024-5-3

    The Agda Wiki. https://wiki.portal.chalmers.se/agda/pmwiki.php, accessed: 2024-5-3

    2024

  20. [28]

    The GNU MP Bignum Library.https://gmplib.org/, accessed: 2024-12-8

    2024

  21. [29]

    Idris: A Language for Type-Driven Development.https://www.idris-lang.org/, accessed: 2024-5-3

    2024

  22. [30]

    Lean: Programming Language and Theorem Prover.https://lean-lang.org/, ac- cessed: 2024-5-3

    2024

  23. [31]

    Welcome to a World of Rocq.https://rocq-prover.org/, accessed: 2025-4-16

    2025

  24. [32]

    https://agda.github.io/ agda2hs/, accessed: 2025-2-19

    agda2hs Documentation — agda2hs documentation. https://agda.github.io/ agda2hs/, accessed: 2025-2-19

    2025

  25. [33]

    Issue #7701.https: //github.com/idris-lang/Idris2/pull/3486, accessed: 2025-2-19 Custom Representations of Inductive Families 25

    Should Agda optimise away the erasure from Vec to List?. Issue #7701.https: //github.com/idris-lang/Idris2/pull/3486, accessed: 2025-2-19 Custom Representations of Inductive Families 25

    2025

  26. [34]

    https://coq.inria.fr/doc/ v8.13/refman/addendum/extraction.html, accessed: 2025-2-19

    Program extraction — Coq 8.13.2 documentation. https://coq.inria.fr/doc/ v8.13/refman/addendum/extraction.html, accessed: 2025-2-19

    2025

  27. [35]

    https://idris2.readthedocs.io/en/ latest/reference/pragmas.html#transform, accessed: 2025-2-19

    Pragmas — Idris2 0.0 documentation. https://idris2.readthedocs.io/en/ latest/reference/pragmas.html#transform, accessed: 2025-2-19

    2025

  28. [36]

    Make ‘CONS’, ‘NIL’, ‘JUST’ and ‘NOTHING’ constructors have uniform names by Z-snails. Pull Request #3486.https://github.com/idris-lang/Idris2/pull/ 3486, accessed: 2025-2-19 26 Constantine Theocharis and Edwin Brady 8 Appendix Implementation The implementation of Superfluid ca...

    2025

  29. [65]

    LICS ’18, Association for Computing Machinery, New York, NY, USA (9 Jul 2018), https://doi.org/10.1145/3209108.3209189

    2018

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.