A Formal Framework for Typing and Cast Semantics in SQL Engines

Practical SQL engines differ in subtle ways in their handling of typing constraints and implicit type casts. These issues, usually not considered in formal accounts of SQL, directly affect the portability of queries between engines. To address this problem, we present a formal typing semantics for SQL, named TRAF , that explicitly captures both static and dynamic type behavior. The system TRAF is expressed in terms of abstract operators that provide the necessary leeway to systematically model the type and cast behavior of different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle). We show that this formalism provides formal guarantees for the handling of types. We identify practical conditions under which engine instantiations satisfy type safety and type soundness. In this regard, TRAF can serve as an explicit and testable account of typing in existing engines, potentially guide their evolution, and provide a formal basis to study type-aware query optimizations and design provably-correct query translators. We also test the adequacy of the formalism by implementing TRAF in Python for these five engines and testing it with synthetic queries, SQLancer++- generated queries, and adapted Spider and Calcite benchmark queries.