next up previous contents
Next: Signature Compatibility Up: Static Semantics Previous: Declaration Typing   Contents

Signature Item Typing

We appeal to a signature item analogue of the $ \mathcal O$ function from the last subsection.

This is the first judgment where we deal with constructor classes, for the $ \mathsf{class}$ forms. We will omit their special handling in this formal specification. Section 6.3 gives an informal description of how constructor classes influence type inference.

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

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

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

$\displaystyle \infer{\Gamma \vdash \mathsf{val} \; x : \tau \leadsto \Gamma, x : \tau}{
\Gamma \vdash \tau :: \mathsf{Type}
}$

$\displaystyle \infer{\Gamma \vdash \mathsf{structure} \; X : S \leadsto \Gamma,...
... \vdash \mathsf{signature} \; X = S \leadsto \Gamma, X = S}{
\Gamma \vdash S
}$

$\displaystyle \infer{\Gamma \vdash \mathsf{include} \; S \leadsto \Gamma, \math...
...dash S
& \Gamma \vdash S \equiv \mathsf{sig} \; \overline{s} \; \mathsf{end}
}$

$\displaystyle \infer{\Gamma \vdash \mathsf{constraint} \; c_1 \sim c_2 \leadsto...
...sim c_2}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa\}
}$

$\displaystyle \infer{\Gamma \vdash \mathsf{class} \; x :: \kappa = c \leadsto \...
...fer{\Gamma \vdash \mathsf{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$



2014-07-14