Using Dependent Types and Tactics to Enable Semantic Optimization of Language-Integrated Queries

Gregory Malecha and Ryan Wisnesky

Semantic optimization -- the use of data integrity constraints to optimize relational queries -- has been well studied but, owing to limitations in how SQL handles constraints, has not often been applied by mainstream RDBMSs. In a language-integrated query setting, however, the query provider is free to rewrite queries before they are executed on an RDBMS. We show, using Coq as our ambient language, how to use dependent types to represent a well known class of constraints -- embedded, implicational dependencies -- and how Coq tactics can be used to implement a particular kind of semantic optimization: tableaux minimization, which minimizes the number of joins required by a query.

coq refinment databases optimization

download source

@inproceedings{malecha2015semantic-optimization,
 author = {Malecha, Gregory and Wisnesky, Ryan},
 title = {Using {D}ependent {T}ypes and {T}actics to {E}nable {S}emantic {O}ptimization of {L}anguage-integrated {Q}ueries},
 booktitle = {Proceedings of the 15th Symposium on Database Programming Languages},
 series = {DBPL 2015},
 year = {2015},
 isbn = {978-1-4503-3902-5},
 location = {Pittsburgh, PA, USA},
 pages = {49--58},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/2815072.2815080},
 doi = {10.1145/2815072.2815080},
 acmid = {2815080},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Chase, Coq, LINQ, semantic optimization},
}