Grain-Aware Data Transformations: Type-Level Formal Verification at Zero Computational Cost

TL;DR

This paper introduces a formal, type-theoretic framework for verifying data transformation correctness at compile time, focusing on data granularity (grain) to prevent errors and reduce verification costs significantly.

Contribution

It extends the concept of data grain into a universal, formal type system, enabling zero-cost, compile-time verification of data pipeline correctness through formal proofs and inference rules.

Findings

Formal definition of data grain in type theory

Proves grain inference theorem for join scenarios

Reduces verification costs by 98-99% with machine-checked proofs

Abstract

Data transformation correctness is a major challenge in data engineering: how to verify pipeline accuracy before deployment. Traditional methods involve costly iterative testing, data materialization, and manual error detection, due to the lack of formal approaches to reasoning about data granularity (grain), which can shift during transformations, causing issues like fan traps (metrics duplication) and chasm traps (data loss). We introduce the first formal, mathematical definition of grain, extending it from an informal concept in dimensional modeling to a universal, type-theoretic framework applicable to any data type. Encoding grain into the type system allows compile-time verification of transformation correctness, shifting validation from runtime. We define three core grain relations-equality, ordering, and incomparability-and prove a general grain inference theorem that computes the output grain of equi-joins from input grains using type-level operations. This covers all join scenarios, including comparable and incomparable keys. Together with inference rules for relational operations, this enables verification through schema analysis alone, at zero cost. Our approach allows engineers to verify that entire pipeline DAGs maintain correctness properties, detecting grain-related errors such as fan traps, chasm traps, and aggregation issues before data processing. It emphasizes the importance of grain, focusing on critical characteristics rather than all data details. We provide machine-checked formal proofs in Lean 4, reducing verification costs by 98-99%. Additionally, large language models can automatically generate correctness proofs, shifting human effort from proof writing to proof verification, thus democratizing formal methods in data engineering and supporting confident deployment of AI-generated pipelines with machine-checkable guarantees.