Queries

A final query is constructed via the $\mathsf{sql\_query}$ function. Constructor arguments respectively specify the unrestricted free table variables (which will only be available in subqueries), the free table variables that may only be mentioned within arguments to aggregate functions, table fields we select (as records mapping tables to the subsets of their fields that we choose), and the (always named) extra expressions that we select.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_query} :: \{\{... ...\; \mathsf{selectedFields} \; \mathsf{selectedExps} \end{array}$$

Queries are used by folding over their results inside transactions.

$$\begin{array}{l} \mathsf{val} \; \mathsf{query} : \mathsf{ta... ...f{state} \to \mathsf{transaction} \; \mathsf{state} \end{array}$$

Most of the complexity of the query encoding is in the type $\mathsf{sql\_query1}$ , which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the unrestricted free table veriables, the aggregate-only free table variables, the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_query1} :: \{\... ...\; \mathsf{selectedFields} \; \mathsf{selectedExps} \end{array}$$

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_query1} : \mat... ...\; \mathsf{selectedFields} \; \mathsf{selectedExps} \end{array}$$

To encode projection of subsets of fields in $\mathsf{SELECT}$ clauses, and to encode $\mathsf{GROUP} \; \mathsf{BY}$ clauses, we rely on a type family $\mathsf{sql\_subset}$ , capturing what it means for one record of table fields to be a subset of another. The main constructor $\mathsf{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mathsf{sql\_subset\_all}$ is a convenience for keeping all fields of a record.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_subset} :: \{\... ...{sql\_subset} \; \mathsf{tables} \; \mathsf{tables} \end{array}$$

SQL expressions are used in several places, including $\mathsf{SELECT}$ , $\mathsf{WHERE}$ , $\mathsf{HAVING}$ , and $\mathsf{ORDER} \; \mathsf{BY}$ clauses. They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places. The arguments to the $\mathsf{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, and the type of the expression.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_exp} :: \{\{\m... ...\mathsf{Type}\} \to \mathsf{Type} \to \mathsf{Type} \end{array}$$

Any field in scope may be converted to an expression.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_field} : \math... ...\mathsf{agg} \; \mathsf{exps} \; \mathsf{fieldType} \end{array}$$

There is an analogous function for referencing named expressions.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_exp} : \mathsf... ...+ \hspace{-.075in} + \;\mathsf{rest}) \; \mathsf{t} \end{array}$$

Ur values of appropriate types may be injected into SQL expressions.

$$\begin{array}{l} \mathsf{class} \; \mathsf{sql\_injectable\_... ...les} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{t} \end{array}$$

Additionally, most function-free types may be injected safely, via the $\mathsf{serialized}$ type family.

$$\begin{array}{l} \mathsf{con} \; \mathsf{serialized} :: \mat... ...table\_prim} \; (\mathsf{serialized} \; \mathsf{t}) \end{array}$$

We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_is\_null} : \m... ...} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{bool} \end{array}$$

As another way of dealing with null values, there is also a restricted form of the standard COALESCE function.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_coalesce} : \m... ...les} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{t} \end{array}$$

We have generic nullary, unary, and binary operators.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_nfunc} :: \mat... ...} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{t} \\ \end{array}$$

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_unary} :: \mat... ...; \mathsf{agg} \; \mathsf{exps} \; \mathsf{res} \\ \end{array}$$

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_binary} :: \ma... ...s} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{res} \end{array}$$

$$\begin{array}{l} \mathsf{class} \; \mathsf{sql\_arith} \\ ... ...ry} \; \mathsf{int} \; \mathsf{int} \; \mathsf{int} \end{array}$$

Finally, we have aggregate functions. The $\mathsf{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument. The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly typed arguments. The key aspect of the $\mathsf{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_count} : \math... ...s} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{int} \end{array}$$

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_aggregate} :: ... ...s} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{ran} \end{array}$$

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_count\_col} : ... ... \; (\mathsf{option} \; \mathsf{t}) \; \mathsf{int} \end{array}$$

Most aggregate functions are typed using a two-parameter constructor class $\mathsf{nullify}$ which maps $\mathsf{option}$ types to themselves and adds $\mathsf{option}$ to others. That is, this constructor class represents the process of making an SQL type ``nullable.''

$$\begin{array}{l} \mathsf{class} \; \mathsf{sql\_summable} \\... ...mathsf{sql\_aggregate} \; \mathsf{t} \; \mathsf{nt} \end{array}$$

$$\begin{array}{l} \mathsf{class} \; \mathsf{sql\_maxable} \\ ... ...mathsf{sql\_aggregate} \; \mathsf{t} \; \mathsf{nt} \end{array}$$

Any SQL query that returns single columns may be turned into a subquery expression.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_subquery} : \ma... ...es} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{nt} \end{array}$$

There is also an IF..THEN..ELSE.. construct that is compiled into standard SQL CASE expressions.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_if\_then\_else}... ...les} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{t} \end{array}$$

FROM clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_from\_items} :... ...athsf{tabs1} + \hspace{-.075in} + \;\mathsf{tabs2}) \end{array}$$

Besides these basic cases, outer joins are supported, which requires a type class for turning non- $\mathsf{option}$ columns into $\mathsf{option}$ columns.

$$\begin{array}{l} \mathsf{class} \; \mathsf{nullify} :: \math... ...y} \; \mathsf{t} \; (\mathsf{option} \; \mathsf{t}) \end{array}$$

Left, right, and full outer joins can now be expressed using functions that accept records of $\mathsf{nullify}$ instances. Here, we give only the type for a left join as an example.

$$\begin{array}{l} \mathsf{val} \; \mathsf{sql\_left\_join} : ... ...ype}) \Rightarrow \mathsf{p}.2)) \; \mathsf{tabs2}) \end{array}$$

We wrap up the definition of query syntax with the types used in representing $\mathsf{ORDER} \; \mathsf{BY}$ , $\mathsf{LIMIT}$ , and $\mathsf{OFFSET}$ clauses.

$$\begin{array}{l} \mathsf{type} \; \mathsf{sql\_direction} \\... ...ql\_offset} : \mathsf{int} \to \mathsf{sql\_offset} \end{array}$$

When using Postgres, SELECT and ORDER BY are allowed to contain top-level uses of window functions. A separate type family sql_expw is provided for such cases, with some type class convenience for overloading between normal and window expressions.

$$\begin{array}{l} \mathsf{con} \; \mathsf{sql\_expw} :: \{\{\... ...s} \; \mathsf{agg} \; \mathsf{exps} \; \mathsf{int} \end{array}$$