Elucidating Type Conversions in SQL Engines

Elucidating Type Conversions in SQL Engines

연구 분야: Databases

학회: European Symposium on Programming

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 , that explicitly captures both static and dynamic type behavior. The system 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, 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 in Python for these five engines, and tested them with thousands of randomly-generated queries.