next up previous contents
Next: Queries Up: SQL Previous: SQL   Contents

Table Declarations

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

\textrm{Declarations} & d &::=& \mathsf...
\textrm{View expressions} & V &::=& Q \mid \{e\}

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.