IC Colloquium : Sound and Efficient Language-Integrated Query: Maintaining the ORDER
Event details
| Date | 11.09.2017 |
| Hour | 16:15 › 17:30 |
| Location | |
| Category | Conferences - Seminars |
By : Oleg Kiselyov - Tohoku University
Video of his talk
Abstract :
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.
Bio :
Oleg Kiselyov is an Assistant Professor in Tohoku University, Japan. He is interested in semantics of programming and natural languages. He worked on continuations, extensible-effects, staging, HList, lightweight dependent types, tagless-final DSL embeddings, macros, non-determinism and logic programming, and probabilistic programming. He is the developer of BER MetaOCaml.
More information
Video of his talk
Abstract :
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.
Bio :
Oleg Kiselyov is an Assistant Professor in Tohoku University, Japan. He is interested in semantics of programming and natural languages. He worked on continuations, extensible-effects, staging, HList, lightweight dependent types, tagless-final DSL embeddings, macros, non-determinism and logic programming, and probabilistic programming. He is the developer of BER MetaOCaml.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host : Martin Odersky