Mercurial > urweb
comparison doc/manual.tex @ 1775:6bc2a8cb3a67
Track whether SQL expressions may use window functions, in preparation for actual window function support
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 02 Jun 2012 15:35:58 -0400 |
parents | 53d56d87fbd2 |
children | 59b07fdae1ff |
comparison
equal
deleted
inserted
replaced
1774:27fdd78bd2f5 | 1775:6bc2a8cb3a67 |
---|---|
1593 \hspace{.1in} \to \mt{sql\_constraint} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine} \rc \mt{munused}) \; [] | 1593 \hspace{.1in} \to \mt{sql\_constraint} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine} \rc \mt{munused}) \; [] |
1594 \end{array}$$ | 1594 \end{array}$$ |
1595 | 1595 |
1596 The last kind of constraint is a \texttt{CHECK} constraint, which attaches a boolean invariant over a row's contents. It is defined using the $\mt{sql\_exp}$ type family, which we discuss in more detail below. | 1596 The last kind of constraint is a \texttt{CHECK} constraint, which attaches a boolean invariant over a row's contents. It is defined using the $\mt{sql\_exp}$ type family, which we discuss in more detail below. |
1597 $$\begin{array}{l} | 1597 $$\begin{array}{l} |
1598 \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] | 1598 \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{disallow\_window} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] |
1599 \end{array}$$ | 1599 \end{array}$$ |
1600 | 1600 |
1601 Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints. There is no other way to use constraints with SQL in Ur/Web. | 1601 Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints. There is no other way to use constraints with SQL in Ur/Web. |
1602 | 1602 |
1603 | 1603 |
1660 \hspace{.1in} \Rightarrow [\mt{free} \sim \mt{grouped}] \\ | 1660 \hspace{.1in} \Rightarrow [\mt{free} \sim \mt{grouped}] \\ |
1661 \hspace{.1in} \Rightarrow [\mt{afree} \sim \mt{tables}] \\ | 1661 \hspace{.1in} \Rightarrow [\mt{afree} \sim \mt{tables}] \\ |
1662 \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\ | 1662 \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\ |
1663 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\ | 1663 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\ |
1664 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\ | 1664 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\ |
1665 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{bool}, \\ | 1665 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{disallow\_window} \; \mt{bool}, \\ |
1666 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ | 1666 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ |
1667 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{bool}, \\ | 1667 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{disallow\_window} \; \mt{bool}, \\ |
1668 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\ | 1668 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\ |
1669 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\ | 1669 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{allow\_window}) \; \mt{selectedExps}) \} \\ |
1670 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} | 1670 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} |
1671 \end{array}$$ | 1671 \end{array}$$ |
1672 | 1672 |
1673 To encode projection of subsets of fields in $\mt{SELECT}$ clauses, and to encode $\mt{GROUP} \; \mt{BY}$ clauses, we rely on a type family $\mt{sql\_subset}$, capturing what it means for one record of table fields to be a subset of another. The main constructor $\mt{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mt{sql\_subset\_all}$ is a convenience for keeping all fields of a record. | 1673 To encode projection of subsets of fields in $\mt{SELECT}$ clauses, and to encode $\mt{GROUP} \; \mt{BY}$ clauses, we rely on a type family $\mt{sql\_subset}$, capturing what it means for one record of table fields to be a subset of another. The main constructor $\mt{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mt{sql\_subset\_all}$ is a convenience for keeping all fields of a record. |
1674 $$\begin{array}{l} | 1674 $$\begin{array}{l} |
1678 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1 \rc \mt{fields}.2)\; \mt{keep\_drop}) \\ | 1678 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1 \rc \mt{fields}.2)\; \mt{keep\_drop}) \\ |
1679 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\ | 1679 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\ |
1680 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables} | 1680 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables} |
1681 \end{array}$$ | 1681 \end{array}$$ |
1682 | 1682 |
1683 SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{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 $\mt{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. | 1683 SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{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 $\mt{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, whether window functions are allowed, and the type of the expression. Two abstract constructors are declared to use to specify window function allowedness. |
1684 $$\begin{array}{l} | 1684 $$\begin{array}{l} |
1685 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} | 1685 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \{\mt{Unit}\} \to \mt{Type} \\ |
1686 \mt{con} \; \mt{disallow\_window} :: \{\mt{Unit}\} \\ | |
1687 \mt{con} \; \mt{allow\_window} :: \{\mt{Unit}\} | |
1686 \end{array}$$ | 1688 \end{array}$$ |
1687 | 1689 |
1688 Any field in scope may be converted to an expression. | 1690 Any field in scope may be converted to an expression. |
1689 $$\begin{array}{l} | 1691 $$\begin{array}{l} |
1690 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\ | 1692 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\ |
1691 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ | 1693 \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ |
1692 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\ | 1694 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\ |
1693 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\ | 1695 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\ |
1694 \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{fieldType} | 1696 \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{fieldType} |
1695 \end{array}$$ | 1697 \end{array}$$ |
1696 | 1698 |
1697 There is an analogous function for referencing named expressions. | 1699 There is an analogous function for referencing named expressions. |
1698 $$\begin{array}{l} | 1700 $$\begin{array}{l} |
1699 \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\ | 1701 \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\ |
1700 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t} | 1702 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{aw} \; \mt{t} |
1701 \end{array}$$ | 1703 \end{array}$$ |
1702 | 1704 |
1703 Ur values of appropriate types may be injected into SQL expressions. | 1705 Ur values of appropriate types may be injected into SQL expressions. |
1704 $$\begin{array}{l} | 1706 $$\begin{array}{l} |
1705 \mt{class} \; \mt{sql\_injectable\_prim} \\ | 1707 \mt{class} \; \mt{sql\_injectable\_prim} \\ |
1714 \\ | 1716 \\ |
1715 \mt{class} \; \mt{sql\_injectable} \\ | 1717 \mt{class} \; \mt{sql\_injectable} \\ |
1716 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\ | 1718 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\ |
1717 \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\ | 1719 \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\ |
1718 \\ | 1720 \\ |
1719 \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ | 1721 \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ |
1720 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} | 1722 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} |
1721 \end{array}$$ | 1723 \end{array}$$ |
1722 | 1724 |
1723 Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family. | 1725 Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family. |
1724 $$\begin{array}{l} | 1726 $$\begin{array}{l} |
1725 \mt{con} \; \mt{serialized} :: \mt{Type} \to \mt{Type} \\ | 1727 \mt{con} \; \mt{serialized} :: \mt{Type} \to \mt{Type} \\ |
1728 \mt{val} \; \mt{sql\_serialized} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{serialized} \; \mt{t}) | 1730 \mt{val} \; \mt{sql\_serialized} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{serialized} \; \mt{t}) |
1729 \end{array}$$ | 1731 \end{array}$$ |
1730 | 1732 |
1731 We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values. | 1733 We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values. |
1732 $$\begin{array}{l} | 1734 $$\begin{array}{l} |
1733 \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ | 1735 \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ |
1734 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} | 1736 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{aw} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} |
1735 \end{array}$$ | 1737 \end{array}$$ |
1736 | 1738 |
1737 As another way of dealing with null values, there is also a restricted form of the standard \cd{COALESCE} function. | 1739 As another way of dealing with null values, there is also a restricted form of the standard \cd{COALESCE} function. |
1738 $$\begin{array}{l} | 1740 $$\begin{array}{l} |
1739 \mt{val} \; \mt{sql\_coalesce} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ | 1741 \mt{val} \; \mt{sql\_coalesce} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ |
1740 \hspace{.1in} \to \mt{t} ::: \mt{Type} \\ | 1742 \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ |
1741 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \\ | 1743 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; (\mt{option} \; \mt{t}) \\ |
1742 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ | 1744 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ |
1743 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} | 1745 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} |
1744 \end{array}$$ | 1746 \end{array}$$ |
1745 | 1747 |
1746 We have generic nullary, unary, and binary operators. | 1748 We have generic nullary, unary, and binary operators. |
1747 $$\begin{array}{l} | 1749 $$\begin{array}{l} |
1748 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\ | 1750 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\ |
1749 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\ | 1751 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\ |
1750 \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ | 1752 \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ |
1751 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$ | 1753 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} |
1754 \end{array}$$ | |
1752 | 1755 |
1753 $$\begin{array}{l} | 1756 $$\begin{array}{l} |
1754 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ | 1757 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ |
1755 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\ | 1758 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\ |
1756 \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ | 1759 \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ |
1757 \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} \\ | 1760 \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res} |
1758 \end{array}$$ | 1761 \end{array}$$ |
1759 | 1762 |
1760 $$\begin{array}{l} | 1763 $$\begin{array}{l} |
1761 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\ | 1764 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\ |
1762 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ | 1765 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ |
1763 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ | 1766 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ |
1764 \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ | 1767 \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ |
1765 \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_1} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_2} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} | 1768 \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ |
1769 \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \\ | |
1770 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_1} \\ | |
1771 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_2} \\ | |
1772 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res} | |
1766 \end{array}$$ | 1773 \end{array}$$ |
1767 | 1774 |
1768 $$\begin{array}{l} | 1775 $$\begin{array}{l} |
1769 \mt{class} \; \mt{sql\_arith} \\ | 1776 \mt{class} \; \mt{sql\_arith} \\ |
1770 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\ | 1777 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\ |
1777 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int} | 1784 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int} |
1778 \end{array}$$ | 1785 \end{array}$$ |
1779 | 1786 |
1780 Finally, we have aggregate functions. The $\mt{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 $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields. | 1787 Finally, we have aggregate functions. The $\mt{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 $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields. |
1781 $$\begin{array}{l} | 1788 $$\begin{array}{l} |
1782 \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int} | 1789 \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \mt{aw} ::: \{\mt{Unit}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{int} |
1783 \end{array}$$ | 1790 \end{array}$$ |
1784 | 1791 |
1785 $$\begin{array}{l} | 1792 $$\begin{array}{l} |
1786 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ | 1793 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ |
1787 \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ | 1794 \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Type}\} \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ |
1788 \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{ran} | 1795 \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{ran} |
1789 \end{array}$$ | 1796 \end{array}$$ |
1790 | 1797 |
1791 $$\begin{array}{l} | 1798 $$\begin{array}{l} |
1792 \mt{val} \; \mt{sql\_count\_col} : \mt{t} ::: \mt{Type} \to \mt{sql\_aggregate} \; (\mt{option} \; \mt{t}) \; \mt{int} | 1799 \mt{val} \; \mt{sql\_count\_col} : \mt{t} ::: \mt{Type} \to \mt{sql\_aggregate} \; (\mt{option} \; \mt{t}) \; \mt{int} |
1793 \end{array}$$ | 1800 \end{array}$$ |
1813 \end{array}$$ | 1820 \end{array}$$ |
1814 | 1821 |
1815 Any SQL query that returns single columns may be turned into a subquery expression. | 1822 Any SQL query that returns single columns may be turned into a subquery expression. |
1816 | 1823 |
1817 $$\begin{array}{l} | 1824 $$\begin{array}{l} |
1818 \mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ | 1825 \mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \\ |
1819 \hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt} | 1826 \hspace{.1in} \to \mt{aw} ::: \mt{Type} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ |
1827 \hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{nt} | |
1820 \end{array}$$ | 1828 \end{array}$$ |
1821 | 1829 |
1822 There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions. | 1830 There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions. |
1823 $$\begin{array}{l} | 1831 $$\begin{array}{l} |
1824 \mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ | 1832 \mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ |
1825 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\ | 1833 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} \\ |
1826 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ | 1834 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ |
1827 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ | 1835 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ |
1828 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} | 1836 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} |
1829 \end{array}$$ | 1837 \end{array}$$ |
1830 | 1838 |
1831 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. | 1839 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. |
1832 $$\begin{array}{l} | 1840 $$\begin{array}{l} |
1833 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ | 1841 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ |
1838 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ | 1846 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ |
1839 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) \\ | 1847 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) \\ |
1840 \mt{val} \; \mt{sql\_inner\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \\ | 1848 \mt{val} \; \mt{sql\_inner\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \\ |
1841 \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ | 1849 \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ |
1842 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ | 1850 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ |
1843 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ | 1851 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\ |
1844 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) | 1852 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) |
1845 \end{array}$$ | 1853 \end{array}$$ |
1846 | 1854 |
1847 Besides these basic cases, outer joins are supported, which requires a type class for turning non-$\mt{option}$ columns into $\mt{option}$ columns. | 1855 Besides these basic cases, outer joins are supported, which requires a type class for turning non-$\mt{option}$ columns into $\mt{option}$ columns. |
1848 $$\begin{array}{l} | 1856 $$\begin{array}{l} |
1856 $$\begin{array}{l} | 1864 $$\begin{array}{l} |
1857 \mt{val} \; \mt{sql\_left\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{(\mt{Type} \times \mt{Type})\}\} \\ | 1865 \mt{val} \; \mt{sql\_left\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{(\mt{Type} \times \mt{Type})\}\} \\ |
1858 \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ | 1866 \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ |
1859 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\lambda \mt{r} \Rightarrow \$(\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{nullify} \; \mt{p}.1 \; \mt{p}.2) \; \mt{r})) \; \mt{tabs2}) \\ | 1867 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\lambda \mt{r} \Rightarrow \$(\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{nullify} \; \mt{p}.1 \; \mt{p}.2) \; \mt{r})) \; \mt{tabs2}) \\ |
1860 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\ | 1868 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\ |
1861 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ | 1869 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\ |
1862 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2}) | 1870 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2}) |
1863 \end{array}$$ | 1871 \end{array}$$ |
1864 | 1872 |
1865 We wrap up the definition of query syntax with the types used in representing $\mt{ORDER} \; \mt{BY}$, $\mt{LIMIT}$, and $\mt{OFFSET}$ clauses. | 1873 We wrap up the definition of query syntax with the types used in representing $\mt{ORDER} \; \mt{BY}$, $\mt{LIMIT}$, and $\mt{OFFSET}$ clauses. |
1866 $$\begin{array}{l} | 1874 $$\begin{array}{l} |
1869 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\ | 1877 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\ |
1870 \\ | 1878 \\ |
1871 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ | 1879 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ |
1872 \mt{val} \; \mt{sql\_order\_by\_Nil} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} :: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ | 1880 \mt{val} \; \mt{sql\_order\_by\_Nil} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} :: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ |
1873 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ | 1881 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ |
1874 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ | 1882 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{allow\_window} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ |
1875 \mt{val} \; \mt{sql\_order\_by\_random} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ | 1883 \mt{val} \; \mt{sql\_order\_by\_random} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ |
1876 \\ | 1884 \\ |
1877 \mt{type} \; \mt{sql\_limit} \\ | 1885 \mt{type} \; \mt{sql\_limit} \\ |
1878 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\ | 1886 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\ |
1879 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\ | 1887 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\ |
1900 \end{array}$$ | 1908 \end{array}$$ |
1901 | 1909 |
1902 Properly-typed records may be used to form $\mt{INSERT}$ commands. | 1910 Properly-typed records may be used to form $\mt{INSERT}$ commands. |
1903 $$\begin{array}{l} | 1911 $$\begin{array}{l} |
1904 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ | 1912 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ |
1905 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml} | 1913 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; [] \; \mt{disallow\_window}) \; \mt{fields}) \to \mt{dml} |
1906 \end{array}$$ | 1914 \end{array}$$ |
1907 | 1915 |
1908 An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause. Note that, in the table environment applied to expressions, the table being updated is hardcoded at the name $\mt{T}$. The parsing extension for $\mt{UPDATE}$ will elaborate all table-free field references to use table variable $\mt{T}$. | 1916 An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause. Note that, in the table environment applied to expressions, the table being updated is hardcoded at the name $\mt{T}$. The parsing extension for $\mt{UPDATE}$ will elaborate all table-free field references to use table variable $\mt{T}$. |
1909 $$\begin{array}{l} | 1917 $$\begin{array}{l} |
1910 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ | 1918 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ |
1911 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ | 1919 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window}) \; \mt{changed}) \\ |
1912 \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml} | 1920 \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml} |
1913 \end{array}$$ | 1921 \end{array}$$ |
1914 | 1922 |
1915 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. The above use of $\mt{T}$ is repeated. | 1923 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. The above use of $\mt{T}$ is repeated. |
1916 $$\begin{array}{l} | 1924 $$\begin{array}{l} |
1917 \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml} | 1925 \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml} |
1918 \end{array}$$ | 1926 \end{array}$$ |
1919 | 1927 |
1920 \subsubsection{Sequences} | 1928 \subsubsection{Sequences} |
1921 | 1929 |
1922 SQL sequences are counters with concurrency control, often used to assign unique IDs. Ur/Web supports them via a simple interface. The only way to create a sequence is with the $\mt{sequence}$ declaration form. | 1930 SQL sequences are counters with concurrency control, often used to assign unique IDs. Ur/Web supports them via a simple interface. The only way to create a sequence is with the $\mt{sequence}$ declaration form. |