Static Semantics

In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.

The notations used here are the standard ones of programming language semantics. They are probably the most effective way to convey this information. At the same time, most Ur/Web users can probably get by without knowing the contents of this section! If you're interested in diving into the details of Ur typing but are unfamiliar with ``inference rule notation,'' I recommend the following book:

Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002.

Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.

• $\Gamma \vdash \kappa$ expresses kind well-formedness.
• $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
• $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well.
• $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
• $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a definitional equality in the world of type theory.
• $\Gamma \vdash e : \tau$ is a standard typing judgment.
• $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
• $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items.
• $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
• $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$ .
• $\Gamma \vdash M : S$ is the module signature checking judgment.
• $\mathsf{proj}(M, \overline{s}, V)$ is a partial function for projecting a signature item from $\overline{s}$ , given the module $M$ that we project from. $V$ may be $\mathsf{con} \; x$ , $\mathsf{datatype} \; x$ , $\mathsf{val} \; x$ , $\mathsf{signature} \; X$ , or $\mathsf{structure} \; X$ . The parameter $M$ is needed because the projected signature item may refer to other items from $\overline{s}$ .
• $\mathsf{selfify}(M, \overline{s})$ adds information to signature items $\overline{s}$ to reflect the fact that we are concerned with the particular module $M$ . This function is overloaded to work over individual signature items as well.