Table Declarations

$\mathsf{table}$ declarations may include constraints, via these grammar rules.

$$\begin{array}{rrcll} \textrm{Declarations} & d &::=& \mathsf... ... \textrm{View expressions} & V &::=& Q \mid \{e\} \end{array}$$

A signature item $\mathsf{table} \; \mathsf{x} : \mathsf{c}$ is actually elaborated into two signature items: $\mathsf{con} \; \mathsf{x\_hidden\_constraints} :: \{\{\mathsf{Unit}\}\}$ and $\mathsf{val} \; \mathsf{x} : \mathsf{sql\_table} \; \mathsf{c} \; \mathsf{x\_hidden\_constraints}$ . This is appropriate for common cases where client code doesn't care which keys a table has. It's also possible to include constraints after a $\mathsf{table}$ signature item, with the same syntax as for $\mathsf{table}$ declarations. This may look like dependent typing, but it's just a convenience. The constraints are type-checked to determine a constructor $u$ to include in $\mathsf{val} \; \mathsf{x} : \mathsf{sql\_table} \; \mathsf{c} \; (u + \hspace{-.075in} + \;\mathsf{x\_hidden\_constraints})$ , and then the expressions are thrown away. Nonetheless, it can be useful for documentation purposes to include table constraint details in signatures. Note that the automatic generation of $\mathsf{x\_hidden\_constraints}$ leads to a kind of free subtyping with respect to which constraints are defined.