Declaration Typing

We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$ , expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$ , when they are known to belong to datatype $x$ with type parameters $\overline{y}$ .

We presuppose the existence of a function $\mathcal O$ , where $\mathcal O(M, \overline{s})$ implements the $\mathsf{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$ . Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mathsf{Type} = M.x$ ), so that the relationship with $M$ is maintained. A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $\overline s$ . We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$ . We write $\mathsf{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.

$$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} \quad \infer{\Gamma... ...ma \vdash d \leadsto \Gamma' & \Gamma' \vdash \overline{d} \leadsto \Gamma'' }$$

$$\infer{\Gamma \vdash \mathsf{con} \; x :: \kappa = c \leadsto \Ga... ...sf{len}(\overline y)} \to \mathsf{Type} \vdash \overline{dc} \leadsto \Gamma' }$$

$$\infer{\Gamma \vdash \mathsf{datatype} \; x = \mathsf{datatype} \... ...}(\overline y)} \to \mathsf{Type} = M.z \vdash \overline{dc} \leadsto \Gamma' }$$

$$\infer{\Gamma \vdash \mathsf{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{ \Gamma \vdash e : \tau }$$

$$\infer{\Gamma \vdash \mathsf{val} \; \mathsf{rec} \; \overline{x ... ...on $\lambda$, optionally preceded by constructor and disjointness $\lambda$s} }$$

$$\infer{\Gamma \vdash \mathsf{structure} \; X : S = M \leadsto \Ga... ...verline{s})}{ \Gamma \vdash M : \mathsf{sig} \; \overline{s} \; \mathsf{end} }$$

$$\infer{\Gamma \vdash \mathsf{signature} \; X = S \leadsto \Gamma, X = S}{ \Gamma \vdash S }$$

$$\infer{\Gamma \vdash \mathsf{open} \; M \leadsto \Gamma, \mathcal... ...verline{s})}{ \Gamma \vdash M : \mathsf{sig} \; \overline{s} \; \mathsf{end} }$$

$$\infer{\Gamma \vdash \mathsf{constraint} \; c_1 \sim c_2 \leadsto... ...verline{s})}{ \Gamma \vdash M : \mathsf{sig} \; \overline{s} \; \mathsf{end} }$$

$$\infer{\Gamma \vdash \mathsf{table} \; x : c \leadsto \Gamma, x :... ...uery} \; [] \; [] \; (\mathsf{map} \; (\lambda \_ \Rightarrow []) \; c') \; c }$$

$$\infer{\Gamma \vdash \mathsf{sequence} \; x \leadsto \Gamma, x : \mathsf{Basis}.\mathsf{sql\_sequence}}{}$$

$$\infer{\Gamma \vdash \mathsf{cookie} \; x : \tau \leadsto \Gamma,... ... \mathsf{style} \; x \leadsto \Gamma, x : \mathsf{Basis}.\mathsf{css\_class}}{}$$

$$\infer{\Gamma \vdash \mathsf{task} \; e_1 = e_2 \leadsto \Gamma}{... ... & \Gamma \vdash e_2 :: \tau \to \mathsf{Basis}.\mathsf{transaction} \; \{\} }$$

$$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{} \q... ...\overline{y}}{ \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' }$$