Sound and Efficient Language-Integrated Query: Maintaining the ORDER
Recorded 11 September 2017 in Lausanne, Vaud, Switzerland
As SQL moved from the English-like language for ad hoc queries by business users to its present status as the universal relational database access, the lack of abstractions and compositionality in the original design is felt more and more acute. Recently added subqueries
and common table expressions compensate, albeit generally inefficiently. The inadequacies of SQL motivated language-integrated query systems such as (T-)LINQ, which offer an applicative, programming-like query language compiled to efficient SQL.
However, the seemingly straightforward ranking operations ORDER BY and LIMIT are not supported efficiently, consistently or at all in SQL subqueries. The SQL standard defines their behavior only when applied to the whole query. Language-integrated query systems do not support
them either: naively extending ranking to subexpressions breaks the distributivity laws of UNION ALL that underlie optimizations and compilation.
We present the first compositional semantics of ORDER BY and LIMIT, which reproduces in the limit the standard-prescribed SQL behavior but also applies to arbitrary composed query expressions and preserves the distributivity laws. We introduce the relational calculus SQUR that
includes ordering and subranging and whose normal forms correspond to efficient, subquery-free SQL. Treating these operations as effects, we describe a type-and-effect system for SQUR and prove its soundness. Our denotational semantics leads to the provably
correctness-preserving normalization-by-evaluation. An implementation of SQUR thus becomes a sound and efficient language-integrated query system maintaining the ORDER.
Watched 44 times.Watch