  Every database system contains a query optimizer that performs query
rewrites. Unfortunately, developing query optimizers remains a highly
challenging task. Part of the challenges comes from the intricacies and rich
features of query languages, which makes reasoning about rewrite rules
difficult. In this paper, we propose a machine-checkable denotational semantics
for SQL, the de facto language for relational database, for rigorously
validating rewrite rules. Unlike previously proposed semantics that are either
non-mechanized or only cover a small amount of SQL language features, our
semantics covers all major features of SQL, including bags, correlated
subqueries, aggregation, and indexes. Our mechanized semantics, called HoTTSQL,
is based on K-Relations and homotopy type theory, where we denote relations as
mathematical functions from tuples to univalent types. We have implemented
HoTTSQL in Coq, which takes only fewer than 300 lines of code and have proved a
wide range of SQL rewrite rules, including those from database research
literature (e.g., magic set rewrites) and real-world query optimizers (e.g.,
subquery elimination). Several of these rewrite rules have never been
previously proven correct. In addition, while query equivalence is generally
undecidable, we have implemented an automated decision procedure using HoTTSQL
for conjunctive queries: a well-studied decidable fragment of SQL that
encompasses many real-world queries.
