Elucidating Type Conversions 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 understand this problem, we present a formal typing semantics for SQL, named $$\textsf{TRAF} $$ TRAF , that explicitly captures both static and dynamic type behavior. The system $$\textsf{TRAF} $$ TRAF is expressed in terms of abstract operators that provide the necessary leeway to precisely model different SQL engines (PostgreSQL, MS SQL Server, MySQL, SQLite, and Oracle). We show that this formalism provides formal guarantees regarding the handling of types. We provide practical conditions on engines to prove type safety and soundness of queries. In this regard, $$\textsf{TRAF} $$ TRAF can serve as precise documentation of typing in existing engines and potentially guide their evolution, as well as provide a formal basis to study type-aware query optimizations, and design provably-correct query translators. Additionally, we test the adequacy of the formalism, implementing $$\textsf{TRAF} $$ TRAF in Python for these five engines, and tested them with thousands of randomly-generated queries.