Lecture 20: Type-Checking for SQLizability

18 March 2010

Review of what LINQ can do in C# to lower the impedance mismatch between general-purpose programming languages and database query languages. Advantages and limitations on this; in particular the possibility of runtime failure, limits of abstraction, and the role of reflection.

One possible route to improving this: introduction of a type and effect system to track behaviour that cannot be represented in SQL. This allows arbitrary use of parametrization and higher-order functions, while providing compile-time guarantees of on-database execution. Outline of proof via a strongly-normalizing rewrite system. Several examples of how this more deeply embeds querying into a functional language, allowing modular construction of code and opening up queries to conventional compiler rewriting as well as SQL database-specific optimisations.

This lecture is based on the work of Ezra Cooper, in particular the following paper:

You can follow his research blog for more on this.

Homework

Please fill out and submit an anonymous feedback questionnaire. Thank you.