Module Typing

We use a helper function $\mathsf{sigOf}$ , which converts declarations and sequences of declarations into their principal signature items and sequences of signature items, respectively.

$$\infer{\Gamma \vdash M : S}{ \Gamma \vdash M : S' & \Gamma \vda... ...ne{d} \leadsto \Gamma' } \quad \infer{\Gamma \vdash X : S}{ X : S \in \Gamma }$$

$$\infer{\Gamma \vdash M.X : S}{ \Gamma \vdash M : \mathsf{sig} \;... ...; \mathsf{end} & \mathsf{proj}(M, \overline{s}, \mathsf{structure} \; X) = S }$$

$$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{ \Gamma \vda... ...ma \vdash S_1 & \Gamma, X : S_1 \vdash S_2 & \Gamma, X : S_1 \vdash M : S_2 }$$

$$\mathsf{sigOf}(\cdot) = \cdot$$

$$\mathsf{sigOf}(s \; \overline{s'}) = \mathsf{sigOf}(s) \; \mathsf{sigOf}(\overline{s'})$$

$$\mathsf{sigOf}(\mathsf{con} \; x :: \kappa = c) = \mathsf{con} \; x :: \kappa = c$$

$$\mathsf{sigOf}(\mathsf{datatype} \; x \; \overline{y} = \overline{dc}) = \mathsf{datatype} \; x \; \overline{y} = \overline{dc}$$

$$\mathsf{sigOf}(\mathsf{datatype} \; x = \mathsf{datatype} \; M.z) = \mathsf{datatype} \; x = \mathsf{datatype} \; M.z$$

$$\mathsf{sigOf}(\mathsf{val} \; x : \tau = e) = \mathsf{val} \; x : \tau$$

$$\mathsf{sigOf}(\mathsf{val} \; \mathsf{rec} \; \overline{x : \tau = e}) = \overline{\mathsf{val} \; x : \tau}$$

$$\mathsf{sigOf}(\mathsf{structure} \; X : S = M) = \mathsf{structure} \; X : S$$

$$\mathsf{sigOf}(\mathsf{signature} \; X = S) = \mathsf{signature} \; X = S$$

$$\mathsf{sigOf}(\mathsf{open} \; M) = \mathsf{include} \; S \textrm{ (where $\Gamma \vdash M : S$)}$$

$$\mathsf{sigOf}(\mathsf{constraint} \; c_1 \sim c_2) = \mathsf{constraint} \; c_1 \sim c_2$$

$$\mathsf{sigOf}(\mathsf{open} \; \mathsf{constraints} \; M) = \cdot$$

$$\mathsf{sigOf}(\mathsf{table} \; x : c) = \mathsf{table} \; x : c$$

$$\mathsf{sigOf}(\mathsf{view} \; x = e) = \mathsf{view} \; x : c \textrm{ (where $\Gamma \vdash e : \mathsf... ...ery} \; [] \; [] \; (\mathsf{map} \; (\lambda \_ \Rightarrow []) \; c') \; c$)}$$

$$\mathsf{sigOf}(\mathsf{sequence} \; x) = \mathsf{sequence} \; x$$

$$\mathsf{sigOf}(\mathsf{cookie} \; x : \tau) = \mathsf{cookie} \; x : \tau$$

$$\mathsf{sigOf}(\mathsf{style} \; x) = \mathsf{style} \; x$$

$$\mathsf{selfify}(M, \cdot) = \cdot$$

$$\mathsf{selfify}(M, s \; \overline{s'}) = \mathsf{selfify}(M, s) \; \mathsf{selfify}(M, \overline{s'})$$

$$\mathsf{selfify}(M, \mathsf{con} \; x :: \kappa) = \mathsf{con} \; x :: \kappa = M.x$$

$$\mathsf{selfify}(M, \mathsf{con} \; x :: \kappa = c) = \mathsf{con} \; x :: \kappa = c$$

$$\mathsf{selfify}(M, \mathsf{datatype} \; x \; \overline{y} = \overline{dc}) = \mathsf{datatype} \; x \; \overline{y} = \mathsf{datatype} \; M.x$$

$$\mathsf{selfify}(M, \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z) = \mathsf{datatype} \; x = \mathsf{datatype} \; M'.z$$

$$\mathsf{selfify}(M, \mathsf{val} \; x : \tau) = \mathsf{val} \; x : \tau$$

$$\mathsf{selfify}(M, \mathsf{structure} \; X : S) = \mathsf{structure} \; X : \mathsf{selfify}(M.X, \overline{s}) \te... ... (where $\Gamma \vdash S \equiv \mathsf{sig} \; \overline{s} \; \mathsf{end}$)}$$

$$\mathsf{selfify}(M, \mathsf{signature} \; X = S) = \mathsf{signature} \; X = S$$

$$\mathsf{selfify}(M, \mathsf{include} \; S) = \mathsf{include} \; S$$

$$\mathsf{selfify}(M, \mathsf{constraint} \; c_1 \sim c_2) = \mathsf{constraint} \; c_1 \sim c_2$$

$$\mathsf{selfify}(M, \mathsf{class} \; x :: \kappa) = \mathsf{class} \; x :: \kappa = M.x$$

$$\mathsf{selfify}(M, \mathsf{class} \; x :: \kappa = c) = \mathsf{class} \; x :: \kappa = c$$