Pith. sign in

REVIEW 4 major objections 4 minor 60 references

Grain Theory: Type-Level Granularity Correctness in Data Pipelines

T0 review · 4 major / 4 minor · reviewed 2026-08-03 · deepseek-v4-flash

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

Pith's one-line read Grain can be formalized as a minimal type isomorphic to a data type, and the grain of an equi-join is computable from input grains by type-level set operations, making fan and chasm traps detectable from the schema alone.

desk verdict The paper's central equi-join grain inference theorem is false, refuted by its own natural-join example, and the foundations collapse into functional dependence; the topic is worth pursuing but this version does not hold up. read the letter →

arxiv 2601.00995 v2 pith:RQWJI7JQ submitted 2026-01-02 cs.DB

Nikos Karayannidis This is my paper · ORCID
classification cs.DB
keywords graingranularityequi-joininferencetype-levelverificationfantrapchasmdatapipelinecorrectnesshomomorphism
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

This paper attempts to turn 'grain' — the level of detail of data — from an informal data-warehousing notion into a formal, type-level property. It defines the grain of a type as a minimal type isomorphic to it, and shows that grain relations (equality, ordering, incomparability) form a bounded lattice. The central result is a theorem that computes the grain of an equi-join result from the input grains using only set operations on types. If the theorem holds, pipeline-correctness checks — including detection of fan traps (metric duplication) and chasm traps (data loss) — can be performed at design time on the schema alone, before any query executes. The author additionally reports machine-checked formal proofs and a decidable algorithm that composes grain lifts across pipeline DAGs.

What carries the argument

The key object is the grain operator G[-], which assigns to each type R a minimal isomorphic type. The carrying mechanism is the equi-join grain inference theorem: it computes G[Res] for a join from G[R1], G[R2], and the join key Jk, splitting into two cases based on whether the portions of the two grains overlapping the join key are comparable by subset inclusion — Case A uses intersection, Case B uses union. The 'grain homomorphism' (grain projection commutes with transformation, and φ(h2∘h1)=φ(h2)∘φ(h1)) is the compositional principle that lets these per-operation formulas apply across entire pipeline DAGs.

What would settle it

Run the natural-join example in Section 5.3.4 (R1=A×B×C with G[R1]=A×B, R2=B×C×D with G[R2]=C×D, joined on B×C) with concrete data and test whether the computed four-field grain A×B×C×D is minimal: if a proper subset such as A×C×D already uniquely identifies every result row, the formula's output is not irreducible and the inference theorem over-approximates.

Watch

Extended reading notes

Core claim

The paper's central claim is that 'grain' is a property of a type, not of a table: for any data type R, its grain G[R] is the simplest type isomorphic to R, carrying only the information needed to uniquely identify elements. On this foundation the paper defines three grain relations — equality, ordering, and incomparability — and proves that they form a bounded lattice whose ordering axioms recover Armstrong's axioms on product types. The main contribution is the equi-join grain inference theorem: for collections CR1 and CR2 joined on a common key Jk, the grain of the result is obtained from G[R1], G[R2], and Jk by type-level union, intersection, and difference, with one formula when the Jk-

Load-bearing premise

The framework assumes that every data type has a well-defined canonical minimal isomorphic type ('grain'), and that comparing grains by the existence of a function between them behaves as a structural subset ordering; if those fail, the lattice, the grain relations, and the join-inference formulas lack a sound basis.

Editorial extensions

If this is right

  • A data engineer can verify a multi-stage pipeline's grain correctness by symbolic computation on schemas alone, without running a single query.
  • Fan traps become schema-detectable: if a join's computed result grain is strictly finer than an input grain, metrics from that input will be duplicated under aggregation.
  • Chasm traps localize to ordering chains where a nullable foreign key makes a grain function partial, guiding the choice between INNER and OUTER JOIN.
  • When grain is encoded in the type system, behavioral-class mistakes (such as point-in-time queries on the wrong collection type) become compile-time type errors.
  • The inference rules cover the full relational algebra — selection, projection, extension, rename, grouping, set operations, theta/semi/anti-joins — so the design-time check applies to arbitrary transformation DAGs, not just single joins.

Reading between the lines

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

  • The grain homomorphism suggests a functorial reading: grain is a structure-preserving map from data types to grains, and pipeline transformations act on grains — a perspective that would let correctness of a composed pipeline be checked stage-by-stage, a step toward compositional verification of large DAGs.
  • A practical adoption path the paper only sketches is encoding grain as phantom types in mainstream languages; a testable extension would measure how many real-world pipeline bugs are actually caught by such encodings on open-source dbt or Spark SQL pipelines.
  • The framework's broad applicability to non-record types (lists, maps, streams) depends on supplying an explicit isomorphism to a grain type that may not be a field of the record; this suggests a metadata/annotation layer is a practical prerequisite for deployment.
  • For cross-system integration, the generalized isomorphic-key theorem implies schema-matching tools could consume grain types directly, converting attribute correspondences into type-level isomorphism witnesses.
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

4 major / 4 minor

Summary. The paper introduces 'grain theory,' a type-theoretic framework for data transformation correctness. It defines grain as a minimal type isomorphic to the data type, introduces grain equality, ordering, and incomparability relations, claims a bounded lattice, and presents a grain inference theorem for equi-joins (Theorem 5.1) with two cases, plus corollaries for equal, ordered, incomparable, and natural joins. The authors further claim a generalized join theorem for isomorphic keys, inference rules for other relational operations, a decidable algorithm CalcG, empirical validation on 100 PostgreSQL examples, and machine-checkable formalization in Lean 4. The central promise is that pipeline correctness can be verified at design time, before data execution.

Significance. If the central equi-join grain inference theorem were correct, the framework would offer a genuinely useful design-time check for fan and chasm traps. The paper also ships substantial artifacts—Lean 4 formalization, encodings in Python/Lean/Agda, and 100 SQL experiments—and makes a concrete economic argument. These are real strengths: the empirical setup is clearly described and the artifact link is provided. However, the correctness of the framework is the load-bearing issue, and the paper's own natural-join example invalidates Theorem 5.1. The foundations in Definitions 3.3 and 4.4 are also not sufficient to support the claimed trichotomy and lattice, and the empirical protocol cannot detect the identified failure. As it stands, the paper's main theoretical claim is false under its own definitions, so the significance is currently negative.

major comments (4)
  1. [Theorem 5.1, Case B / Corollary 5.5] The Case B formula is contradicted by the paper's own natural-join example in Corollary 5.5. There, R1=A×B×C with G[R1]=A×B and R2=B×C×D with G[R2]=C×D, so Jk=B×C, G_Jk_1=B, G_Jk_2=C. Case B gives G[Res]=A×D×B×C. But A×C×D already uniquely determines every join row: from (a,c,d), the key (C,D) of R2 determines the unique R2 row, hence B; then the key (A,B) of R1 determines the unique R1 row. A×B×D is symmetric. Thus the claimed result grain is a reducible superkey, violating Definition 3.3's irreducibility. The Appendix N proof only checks that omitting G_rest1, G_rest2, or the common Jk portion breaks uniqueness; it never tests omitting one side's Jk-unique field when the other side's key plus join equality determines it. This is a load-bearing error: Theorem 5.1 is the main technical contribution.
  2. [Definitions 3.3 and 4.4] The definition of grain as a 'canonical minimal representative' of an isomorphism class is not mathematically well-defined in general. For countably infinite types, all countably infinite sets are isomorphic, so grain collapses to cardinality and irreducibility is trivial. For finite types, the Customer→CustomerId example requires an instance-level functional dependency from CustomerId to Name/Email, which is exactly the kind of data-dependent constraint the abstract claims to avoid. Moreover, Definition 4.4 defines grain ordering by 'there exists a function G[R1]→G[R2]'; under standard set-theoretic semantics, any two nonempty types are comparable in this order (choose a constant function), so the equality/ordering/incomparability trichotomy and the lattice of Section 4.5 lack a sound basis. These are not merely presentation issues; they undermine the claimed generality and the join the
  3. [Section 5.6, verification protocol] The empirical validation is circular for the property that matters. Step 4 creates a PRIMARY KEY on the predicted grain before Step 5 checks COUNT(*)=COUNT(DISTINCT G[Res]); the constraint itself forces the counts to match, so the experiment only tests the tautology that a key is a key. More importantly, no test checks irreducibility/minimality. The Case B counterexample above would pass this protocol: A×B×C×D is a valid primary key even though A×C×D is a smaller key. Thus the reported '100% accuracy' cannot detect the central failure of Theorem 5.1. The protocol also silently assumes the generated data satisfies the implicit completeness/'fullness' assumptions behind the grain assignments; the paper does not state or test those assumptions.
  4. [Abstract and Section 6.1.3, Lean 4 claim] The abstract states that 'all theorems are mechanically verified in Lean 4' and Section 6.1.3 claims formal proofs of the three pipeline alternatives. Since Theorem 5.1 is false as stated, no sound Lean 4 proof of that theorem can exist. Either the Lean formalization proves a different statement (e.g., a restricted version with additional assumptions not in the paper), or the artifact does not cover the theorem as written. The paper gives no Lean source snippets and no details of the formalized grain relation or join theorem, so a reader cannot tell which is the case. This needs to be clarified before the formal-verification claim can be assessed.
minor comments (4)
  1. [Throughout] Typographical issues: 'Eqi-Joins' in Theorem 5.1, 'Eqality' in Theorem 4.2, and inconsistent corollary numbering between the main text and the appendix (e.g., 'Corollary 11.1/11.2/11.3' in Appendix O-R). These should be fixed.
  2. [Section 4.5, Figure 1] The lattice figure is described but not shown in the text. The description of glb as union and lub as intersection is also stated without proof; given the ordering issues in Definition 4.4, Figure 1 would need a corrected ordering relation to be meaningful.
  3. [Section 6.3] The cost-benefit analysis depends on free parameters: per-bug debugging iterations (3–7), compute cost ($5–$50), engineer time (4–12 h), and bug rate (0.25–1 per pipeline). The sensitivity analysis is presented, but the assumption that '1 grain bug per pipeline' is 'conservative' is not justified. This does not affect the main technical claim but should be labeled as an illustrative estimate.
  4. [Section 5.6 / Table 3] The verification section says the experiments are complementary to the formal proof, but the paper never identifies what the Lean artifacts actually contain. A small appendix listing the Lean declarations for grain and join inference, or a link to a specific file, would help.

Circularity Check

1 steps flagged · score 6.0 of 10

Empirical verification of the join-grain formula is circular: the predicted grain is installed as the result table's PRIMARY KEY, so the subsequent uniqueness check is guaranteed by schema, and the defining irreducibility property is never tested.

  1. self definitional [Section 5.6 and 5.6.1 (Constraint Verification / Uniqueness Validation)]
    "Each example follows a rigorous verification protocol: we compute the expected grain using the appropriate formula, create result tables with PRIMARY KEY constraints on the calculated grain columns, and verify that COUNT(*)=COUNT(DISTINCT G[Res]) to confirm the grain uniquely identifies all result rows."

    The predicted grain is imposed as the table's PRIMARY KEY before the check is run; a primary key by definition makes COUNT(DISTINCT cols)=COUNT(*) for any table that accepts the insert. The only property tested is uniqueness, and even that is enforced by the schema rather than independently measured. Definition 3.3 defines grain by isomorphism plus irreducibility ('No proper subset of G[R] can serve as the grain of R'), but the protocol never checks minimality. Thus the claimed '100% formula accuracy' reduces to checking that a self-imposed superkey is a superkey on data generated from the same grain declarations; it cannot detect the paper's own Case B counterexample, where the formula returns a reducible key.

full rationale

The paper contains a substantial independent (though apparently unsound) derivation: grain is defined by isomorphism and irreducibility, and Theorem 5.1 attempts to compute join grains from input grains. That derivation is not circular in the sense of assuming its own conclusion; its Case B error is a mathematical gap, not a definitional reduction. There are no load-bearing self-citations. The circularity I find is in the empirical verification protocol (Section 5.6): the expected grain is built into the result table as a PRIMARY KEY before the uniqueness check, making the COUNT(*)=COUNT(DISTINCT ...) test tautological, and the defining irreducibility requirement is never tested. The experiment therefore cannot distinguish the theorem's formula from a merely weaker superkey claim and mirrors the synthetic data-generation assumptions. Armstrong's axioms are explicitly imported ('We treat ≤_g as a functional dependency relation at the type level'), so 'recovering' them is a renaming rather than a derivation, but this is not load-bearing for the join theorem. Overall score reflects one central validation step that reduces by construction, not a fully circular derivation.

Assumptions & free parameters 3 free parameters · 4 assumptions · 3 invented entities

The central framework rests on the axiom that grain is a well-defined type-level object: a minimal type isomorphic to R (Definition 3.3). For plain sets this is either vacuous (any two countably infinite sets are isomorphic, so grain reduces to cardinality) or silently instance-constrained (Customer→CustomerId holds only if each id determines exactly one name/email — a hidden FD). The ordering (Definition 4.4) is stated as existence of an arbitrary function, which is nearly always true for nonempty types, so the trichotomy and lattice degenerate without an unstated structural-projection reading. The corollaries add an ad hoc identification of ≡_g with type equality (Appendix P), contradicting §5.3.1; the natural-join Case B computation violates the theorem's own bound and yields a non-minimal grain. These are load-bearing premises, not typos: without each, the inference rules and verification claims collapse.

free parameters (3)
  • cost-model inputs (per-bug debugging iterations 3–7; compute cost $5–$50 per run; engineer time 4–12 h; bug rate 0.25–1 = $415–$2,750 per bug; $8–$50 per pipeline; 98–99% reduction
    These numbers are asserted in §6.1.3 and §6.3 with no measured data; they are hand-chosen inputs to the claimed cost reduction and are not derived from any experiment.
  • assumed instance 'fullness' for the 100 PostgreSQL examples = 1,000+ rows per table; all examples pass
    Generated data is constructed to match the predicted grain; the protocol (§5.6) forces uniqueness by making the predicted grain a PRIMARY KEY, so the check is satisfied by construction and never tests minimality.
  • implicit instance constraints behind grain examples = G[Customer]=CustomerId (one name/email per id)
    The examples require the instance sets to satisfy hidden FDs; without them the isomorphism in Definition 3.3 fails for plain product types.
assumptions (4)
  • standard math Sets are interpreted as plain types; a function A→B exists whenever B is nonempty (standard set theory).
    Used in Definition 4.4; under this reading grain ordering is nearly universal on nonempty types and the three-relation trichotomy degenerates — the intended structural-projection reading is never stated.
  • domain assumption Every relation instance is 'full': type-level grain implies instance-level uniqueness and multiplicity.
    The Metrics Duplication Rule ('G[Res]<_g G[Ri] ⇒ metrics from Ri are duplicated', §6.1.2) is treated as formally proven, but type-level ordering only gives a possibility, not actual row multiplicities, unless instances are assumed complete.
  • ad hoc to paper G[R1]≡_g G[R2] implies G[R1]=G[R2] as types.
    Assumed in the Equal Grains corollary proof (Appendix P: 'we have G[R1]=G[R2] (as types)'), directly contradicting the paper's own note in §5.3.1 that ≡_g means isomorphism, not identity.
  • ad hoc to paper Isomorphism classes of types have canonical minimal representatives (the grain factors all isomorphic representations).
    The 'categorical interpretation' in §3.2 asserts a universal property over the isomorphism class with no proof; for plain sets the isomorphism class of countable types has no initial/terminal object.
invented entities (3)
  • grain lift φ(h) with homomorphism φ(h2∘h1)=φ(h2)∘φ(h1)
    purpose: Abstract's central 'grain homomorphism' tying join inference to composition over pipeline DAGs.
    Never stated as a theorem or proven in the body; only appears in the abstract. The natural-join counterexample shows the underlying join formula is not even correct.
  • entity key EK and behavioral classes BC[R] (type-level triple (G,EK,BC))
    purpose: Abstract contribution list; behavioral classes would make point-in-time misuse a compile-time error.
    EK is deferred to future work in §7.5 and BC only appears in the abstract; neither is defined or used in the paper.
  • CalcG decidable algorithm
    purpose: Composes grain lifts across pipeline DAGs (abstract).
    Mentioned only in the arXiv abstract; no algorithm, pseudocode, or complexity analysis appears in the full text.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Grain Theory: Type-Level Granularity Correctness in Data Pipelines." pith.science (2026). https://pith.science/paper/RQWJI7JQ

@misc{pith2026260100995,
  author       = {Pith},
  title        = {Pith review of: Grain Theory: Type-Level Granularity Correctness in Data Pipelines},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RQWJI7JQ}},
  note         = {Machine review of arXiv:2601.00995}
}
abstract

Data transformation correctness is a fundamental challenge in data engineering: how can we verify that pipelines produce correct results before executing on production data? Existing practice relies on iterative testing over materialized data. A common cause of errors is the absence of formal reasoning about grain -- the level of detail of data -- so transformations inadvertently change granularity, yielding pathologies like fan traps (metric duplication) and chasm traps (data loss). We introduce grain theory, a type-theoretic framework that elevates grain to a composable property of any algebraic data type. It has two phases. First, a denotation of data: grain itself, defined by irreducibility and isomorphism, with no reference to functional dependencies; three grain relations forming a bounded lattice whose axioms recover Armstrong's on product types; the entity key as a derived grain; and grain-determined behavioral classes -- together the type-level triple (G[R], EK[R], BC[R]). Second, a denotation of transformations: every transformation $h$ has a grain lift $\varphi(h)$. For collections of product types under the relational algebra we prove an equi-join grain inference theorem and present CalcG, a decidable algorithm that composes grain lifts across a pipeline DAG. The central theorem -- the grain homomorphism -- ties the phases together: grain projection commutes with transformation, and grain lifts compose ($\varphi(h_2 \circ h_1) = \varphi(h_2) \circ \varphi(h_1)$). Grain-correctness is therefore verifiable at design time, before any code or query runs. As corollaries, fan traps emerge as schema-detectable grain-relation violations; chasm traps localize to a specific ordering-chain pattern; and behavioral-class violations, such as point-in-time queries on the wrong collection type, become compile-time type errors. All theorems are mechanically verified in Lean 4.

Figures

Figures reproduced from arXiv: 2601.00995 by the authors.

Figure 1
Figure 1. The bounded lattice of the ≤𝑔 partial order relation for four types 𝐴, 𝐵, 𝐶, 𝐷. Definition 4.10 (Grain Incomparability). Given two data types 𝑅1 and 𝑅2, we say they are grain-incomparable and write 𝑅1 ⟨⟩𝑔𝑅2 if and only if: • ¬(𝑅1 ≡𝑔 𝑅2) (not equal) • ¬(𝑅1 ≤𝑔 𝑅2) (not ordered) • ¬(𝑅2 ≤𝑔 𝑅1) (not ordered in reverse) Theorem 4.11 (Grain Incomparability Preservation). Given two data types 𝑅1 and 𝑅2: 𝑅1 ⟨⟩𝑔𝑅2 ⇔ 𝐺[𝑅1] ⟨⟩𝑔… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

60 extracted references · 5 linked inside Pith

  1. [1]

    Chasm Trap problem in Data Warehouses

    2019. Chasm Trap problem in Data Warehouses. https://www.databasesystems. info/2019/02/chasm-trap-problem-in-data-warehouses.html. Accessed: Decem- ber 2024

    2019

  2. [2]

    2 Common SQL Join Traps (with Test Queries)

    2024. 2 Common SQL Join Traps (with Test Queries). https://dataedo.com/blog/2- common-sql-join-traps-with-test-queries. Accessed: December 2024

    2024

  3. [3]

    Escaping SQL Traps with the Unified Star Schema

    2024. Escaping SQL Traps with the Unified Star Schema. https://showmethedata. blog/sql-traps-unified-star-schema. Accessed: December 2024

    2024

  4. [4]

    Ziawasch Abedjan, Lukasz Golab, Felix Naumann, and Thorsten Papenbrock

  5. [5]

    Apache Software Foundation. 2024. Apache Airflow: Platform to program- matically author, schedule and monitor workflows. https://airflow.apache.org/. Accessed: December 2024

    2024

  6. [6]

    Armstrong

    William W. Armstrong. 1974. Dependency structures of data base relationships. InInformation Processing 74: Proceedings of IFIP Congress. North-Holland, 580– 583

    1974

  7. [7]

    Jiang, Jia Deng, Stella Biderman, and Sean Welleck

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck

  8. [8]

    2013.Idris, a general-purpose dependently typed programming language: Design and implementation

    Edwin Brady. 2013.Idris, a general-purpose dependently typed programming language: Design and implementation. Vol. 23. Cambridge University Press. 552– 593 pages

    2013

Show all 60 references
  1. [9]

    Surajit Chaudhuri and Moshe Y. Vardi. 2014. Automated verification of SQL queries.ACM SIGMOD Record43, 2 (2014), 5–17

    2014

  2. [10]

    James Cheney, Sam Lindley, and Philip Wadler. 2013. A practical theory of language-integrated query. InACM SIGPLAN Notices, Vol. 48. ACM, 403–416

    2013

  3. [11]

    2012.Data Matching: Concepts and Techniques for Record Linkage, Entity Resolution, and Duplicate Detection

    Peter Christen. 2012.Data Matching: Concepts and Techniques for Record Linkage, Entity Resolution, and Duplicate Detection. Springer

    2012

  4. [12]

    Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2021. Foun- dations of Fine-Grained Explainability. InProceedings of the VLDB Endowment, Vol. 14. 2537–2550

    2021

  5. [13]

    Ilyas, and Paolo Papotti

    Xu Chu, Ihab F. Ilyas, and Paolo Papotti. 2013. Holistic data cleaning: Putting violations into context. InProceedings of the 2013 ACM SIGMOD International Conference on Management of Data. ACM, 1171–1182

    2013

  6. [14]

    Eric Daimler and Ryan Wisnesky. 2020. Informal Data Transformation Consid- ered Harmful. arXiv:2001.00338 [cs.DB] https://arxiv.org/abs/2001.00338

    2020 arXiv

  7. [15]

    Databricks Inc. 2024. Databricks: Unified Analytics Platform. https://databricks. com/. Accessed: December 2024

    2024

  8. [16]

    dbt Labs. 2024. dbt: Transform data in your warehouse. https://www.getdbt.com/. Accessed: 2024

    2024

  9. [17]

    dbt Labs. 2024. Why should we avoid joins between fact tables? And what are some potential solutions for cross-process analysis? https://github.com/dbt- labs/dbt-technical-blog-writing/discussions/55. Accessed: December 2024

    2024

  10. [18]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. https://leanprover.github.io/. Accessed: 2024

    2021

  11. [19]

    AnHai Doan, Pedro Domingos, and Alon Y. Halevy. 2003. Learning to match the schemas of data sources: A multistrategy approach. InMachine Learning, Vol. 50. Springer, 279–301

    2003

  12. [20]

    Elmagarmid, Panagiotis G

    Ahmed K. Elmagarmid, Panagiotis G. Ipeirotis, and Vassilios S. Verykios. 2007. Duplicate record detection: A survey.IEEE Transactions on Knowledge and Data Engineering19, 1 (2007), 1–16

    2007

  13. [21]

    Kolaitis, Lucian Popa, and Wang-Chiew Tan

    Ronald Fagin, Phokion G. Kolaitis, Lucian Popa, and Wang-Chiew Tan. 2005. Composing schema mappings: Second-order dependencies to the rescue.ACM Transactions on Database Systems30, 4 (2005), 994–1055

    2005

  14. [22]

    Wenfei Fan, Floris Geerts, Jixue Li, and Ming Xiong. 2009. Discovering condi- tional functional dependencies. InProceedings of the 2009 IEEE 25th International Conference on Data Engineering. IEEE, 1231–1234

    2009

  15. [23]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole- proof generation and repair with large language models.Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering(2023), 1229–1241

    2023

  16. [24]

    Google Cloud. 2024. BigQuery: Serverless, highly scalable, and cost-effective multicloud data warehouse. https://cloud.google.com/bigquery. Accessed: December 2024

    2024

  17. [25]

    Great Expectations. 2024. Great Expectations: Always know what to expect from your data. https://greatexpectations.io/. Accessed: December 2024

    2024

  18. [26]

    Venky Harinarayan, Anand Rajaraman, and Jeffrey D. Ullman. 1996. Implement- ing Data Cubes Efficiently. InProceedings of the 1996 ACM SIGMOD Interna- tional Conference on Management of Data, Montreal, Quebec, Canada, June 4-6, 1996, H. V. Jagadish and Inderpal Singh Mumick (Ed...

    1996

  19. [27]

    Benedikt Heinrich, Dessi Hristova, Darya Mirylenka, and Matthias Weidlich

  20. [28]

    Andrew J. Kennedy. 1994. Dimension types.Programming Languages and Systems—ESOP ’94(1994), 348–362. Grain-Aware Data Transformations: Type-Level Formal Verification at Zero Computational Cost

    1994

  21. [29]

    1996.The Data Warehouse Toolkit: Practical Techniques for Building Dimensional Data Warehouses

    Ralph Kimball. 1996.The Data Warehouse Toolkit: Practical Techniques for Building Dimensional Data Warehouses. John Wiley & Sons

    1996

  22. [30]

    Kimball Group. 2024. Dimensional Modeling Techniques. https://www. kimballgroup.com/data-warehouse-business-intelligence-resources/kimball- techniques/dimensional-modeling-techniques/. Accessed: December 2024

    2024

  23. [31]

    Jukka Lehtosalo et al. 2024. mypy: Optional Static Typing for Python. https: //mypy-lang.org/. Accessed: 2024

    2024

  24. [32]

    Daan Leijen and Erik Meijer. 1999. Domain specific embedded compilers. In Proceedings of the 2nd Conference on Domain-Specific Languages. ACM, 109–122

    1999

  25. [33]

    2004.Elements of Finite Model Theory

    Leonid Libkin. 2004.Elements of Finite Model Theory. Springer. Chapter on Data Exchange

    2004

  26. [34]

    1998.Categories for the Working Mathematician(2nd ed.)

    Saunders Mac Lane. 1998.Categories for the Working Mathematician(2nd ed.). Springer

    1998

  27. [35]

    Bernstein, and Erhard Rahm

    Jayant Madhavan, Philip A. Bernstein, and Erhard Rahm. 2001. Generic schema matching with Cupid. InProceedings of the 27th International Conference on Very Large Data Bases. Morgan Kaufmann, 49–58

    2001

  28. [36]

    1984.Intuitionistic Type Theory

    Per Martin-Löf. 1984.Intuitionistic Type Theory. Bibliopolis

    1984

  29. [37]

    Thomas Neumann and Bernhard Radke. 2020. Adaptive optimization of very large join queries. InProceedings of the 2020 ACM SIGMOD International Conference on Management of Data. ACM, 677–692

    2020

  30. [38]

    2014.Programming in Scala: A Comprehensive Step-by-Step Guide

    Martin Odersky, Lex Spoon, and Bill Venners. 2014.Programming in Scala: A Comprehensive Step-by-Step Guide. Artima

    2014

  31. [39]

    Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields

  32. [40]

    Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Wash- burn. 2006. Simple unification-based type inference for GADTs. InACM SIGPLAN Notices, Vol. 41. ACM, 50–61

    2006

  33. [41]

    Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 522–538

    2016

  34. [42]

    François Pottier and Vincent Simonet. 2002. Information flow inference for ML. InProceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 319–330

    2002

  35. [43]

    Bernstein

    Erhard Rahm and Philip A. Bernstein. 2001. A survey of approaches to automatic schema matching.The VLDB Journal10, 4 (2001), 334–350

    2001

  36. [44]

    Robert Rosebrugh and Richard J. Wood. 2000. Relational databases and indexed categories.Electronic Notes in Theoretical Computer Science39, 1 (2000), 1–23

    2000

  37. [45]

    Sebastian Schelter, Dustin Lange, Philipp Schmidt, Meltem Celikel, Felix Biess- mann, and Andreas Grafberger. 2018. Automating large-scale data quality ver- ification. InProceedings of the VLDB Endowment, Vol. 11. VLDB Endowment, 1781–1794

    2018

  38. [46]

    Spivak, and Ryan Wisnesky

    Patrick Schultz, David I. Spivak, and Ryan Wisnesky. 2023. Algebraic Model Management: A Survey.arXiv preprint arXiv:2301.04846(2023)

    2023 arXiv

  39. [47]

    Patrick Schultz and Ryan Wisnesky. 2017. Algebraic Data Integration.Journal of Functional Programming27 (2017), e24. arXiv:1503.03571

    2017 arXiv

  40. [48]

    Pavel Shvaiko and Jérôme Euzenat. 2013. Ontology matching: State of the art and future challenges.IEEE Transactions on Knowledge and Data Engineering25, 1 (2013), 158–176

    2013

  41. [49]

    Siek and Walid Taha

    Jeremy G. Siek and Walid Taha. 2007. Gradual typing for objects. InEuropean Conference on Object-Oriented Programming. Springer, 2–27

    2007

  42. [50]

    Sisense. 2024. Chasm and Fan Traps. https://docs.sisense.com/main/ SisenseLinux/chasm-and-fan-traps.htm. Accessed: December 2024

    2024

  43. [51]

    Snowflake Inc. 2024. Snowflake: The Data Cloud. https://www.snowflake.com/. Accessed: December 2024

    2024

  44. [52]

    Armando Solar-Lezama. 2020. Program synthesis by sketching. InCommunica- tions of the ACM, Vol. 63. ACM, 38–44

    2020

  45. [53]

    David I. Spivak. 2012. Functorial data migration.Information and Computation 217 (2012), 31–51

    2012

  46. [54]

    Agda Development Team. 2024. Agda: A dependently typed functional program- ming language. https://agda.readthedocs.io/. Accessed: 2024

    2024

  47. [55]

    ThoughtSpot. 2024. Chasm traps. https://docs.thoughtspot.com/cloud/latest/ chasm-trap.html. Accessed: December 2024

    2024

  48. [56]

    coarsened

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shix- ing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2024. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models.arXiv preprint arXiv:2306.15626(2024). This appendix contains the formal p...

    2024 arXiv

  49. [2007]

    InJournal of Functional Programming, Vol

    Practical type inference for arbitrary-rank types. InJournal of Functional Programming, Vol. 17. Cambridge University Press, 1–82

  50. [2017]

    InProceedings of the 2017 ACM SIGMOD Interna- tional Conference on Management of Data

    Data profiling: A tutorial. InProceedings of the 2017 ACM SIGMOD Interna- tional Conference on Management of Data. ACM, 1747–1751

    2017

  51. [2018]

    InProceedings of the 2018 International Conference on Management of Data

    Rule-based data quality assessment and monitoring. InProceedings of the 2018 International Conference on Management of Data. ACM, 219–234

    2018

  52. [2023]

    Llemma: An open language model for mathematics.arXiv preprint arXiv:2310.10631(2023)

    2023 arXiv

Pith tools

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