Immutable-record subtyping and bounded quantification

This section records the exact immutable-record and bounded-subtyping systems. The fixed records at the end of the preceding section were a static boundary for $F_{\omega }$ and had no reduction rules. The records below instead belong to an immutable call-by-value calculus. They are finite maps at both the type and term levels, and their fields evaluate in a fixed total order. Thus this section does not add dynamics to the preceding $F_{\omega }$ fragment.

The first-order declarative calculus

The complete first-order type grammar is The index set $I$ is finite, displayed labels are distinct, and reordering a display does not change the finite map. The first-order context $\mathrm{\Gamma }$ contains term declarations only. All rules below are schemas over well-formed types. Formation of the complete grammar is

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢\mathsf{Top}\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢\mathsf{Bot}\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢\mathsf{Unit}\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢\mathsf{Bool}\mathsf{type}$

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢\mathsf{Nat}\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$

$\mathrm{\Gamma }⊢A\to B\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$

$\mathrm{\Gamma }⊢A\times B\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{type}$$\mathrm{\Gamma }⊢B\mathsf{type}$

$\mathrm{\Gamma }⊢A+B\mathsf{type}$

$\mathrm{\Gamma }⊢A_i\mathsf{type}\text{for every }i\in I$

$\mathrm{\Gamma }⊢\{{\ell }_i:A_i{\}}_{i\in I}\mathsf{type}$

The declarative subtype judgment is .

$\mathrm{\Gamma }⊢A\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{type}$

$J\subseteq I$

The term grammar is the inherited explicitly typed call-by-value grammar with the delta The natural-number typing delta is

$\mathrm{\Gamma }⊢0:\mathsf{Nat}$

$\mathrm{\Gamma }⊢t:\mathsf{Nat}$

$\mathrm{\Gamma }⊢\mathsf{suc}(t):\mathsf{Nat}$

$\mathrm{\Gamma }⊢t:\mathsf{Nat}$$\mathrm{\Gamma }⊢t_0:A$$\mathrm{\Gamma },x:\mathsf{Nat},y:A⊢t_s:A$

$\mathrm{\Gamma }⊢\mathsf{natrec}(t;t_0;x.y.t_s):A$

Subsumption, record introduction, and projection are exactly

$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma }⊢t:B$

$\mathrm{\Gamma }⊢t_i:A_i\text{for every }i\in I$

$\mathrm{\Gamma }⊢\{{\ell }_i=t_i{\}}_{i\in I}:\{{\ell }_i:A_i{\}}_{i\in I}$

$\mathrm{\Gamma }⊢t:\{{\ell }_i:A_i{\}}_{i\in I}$$k\in I$

$\mathrm{\Gamma }⊢t.{\ell }_k:A_k$

Natural-number evaluation adds the two congruences and two roots

$t⟶t^{\prime }$

$\mathsf{suc}(t)⟶\mathsf{suc}(t^{\prime })$

$t⟶t^{\prime }$

$\mathsf{natrec}(t;t_0;x.y.t_s)⟶\mathsf{natrec}(t^{\prime };t_0;x.y.t_s)$

$\mathsf{natrec}(0;t_0;x.y.t_s)⟶t_0$

$\mathsf{natrec}(\mathsf{suc}(v);t_0;x.y.t_s)⟶t_s[x\mapsto v,y\mapsto \mathsf{natrec}(v;t_0;x.y.t_s)]$

Record evaluation adds the following three rules. In E-Rcd, refers to the fixed total order of labels.

$t_k⟶t_k^{\prime }$

$\{\dots ,{\ell }_k=t_k,\dots \}⟶\{\dots ,{\ell }_k=t_k^{\prime },\dots \}$

$k\in I$

$\{{\ell }_i=v_i{\}}_{i\in I}.{\ell }_k⟶v_k$

$t⟶t^{\prime }$

$t.{\ell }_k⟶t^{\prime }.{\ell }_k$

There is no runtime form and no reduction rule for subsumption.

Kernel bounded quantification

Kernel extends precisely the grammar above by Contexts now mix term declarations and type bounds. Every declaration is checked in the prefix to its left, so a newly declared $X$ cannot occur in its own bound. Lookup of a type bound is written $\mathrm{\Gamma }(X)=A$.

$\cdot \mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma },x:A\mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Gamma }⊢A\mathsf{type}$$X\notin \mathrm{dom}(\mathrm{\Gamma })$

Type-variable and bounded-universal formation are

$\mathrm{\Gamma }(X)=A$

$\mathrm{\Gamma }⊢X\mathsf{type}$

$\mathrm{\Gamma }⊢A\mathsf{type}$

The Kernel subtype and term rules added to the first-order tables are

$\mathrm{\Gamma }(X)=A$

$\mathrm{\Gamma }⊢t[C]:B[C/X]$

The two bounds in S-AllK are the same constructor modulo alpha-equivalence; the rule does not compare distinct bounds.

Type abstractions are values, type application evaluates its operator, and the one new root contraction is

The deterministic Kernel algorithm

The judgment is read by priority: test alpha-equality, then a top target, then a bottom source, then source-variable promotion, and only then matching outer constructors. A universal comparison fails when its two bounds are not alpha-identical. The following guards make that priority part of the derivation rather than an unstated implementation convention.

$A{\equiv }_{\alpha }B$

$A{\not\equiv }_{\alpha }\mathsf{Top}$

$B{\not\equiv }_{\alpha }\mathsf{Bot}$$B{\not\equiv }_{\alpha }\mathsf{Top}$

$X{\not\equiv }_{\alpha }B$$B{\not\equiv }_{\alpha }\mathsf{Top}$$\mathrm{\Gamma }(X)=U$

$A_1\to A_2{\not\equiv }_{\alpha }{B}_1\to B_2$

$A_1\times A_2{\not\equiv }_{\alpha }{B}_1\times B_2$

$A_1+A_2{\not\equiv }_{\alpha }{B}_1+B_2$

$\{{\ell }_i:A_i{\}}_{i\in I}{\not\equiv }_{\alpha }\{{\ell }_j:B_j{\}}_{j\in J}$$J\subseteq I$

For records, target labels and their recursive premises are visited in the fixed label order. There is no target-promotion rule and no algorithmic transitivity rule.

Boundary table: full is a replacement system

Full omits bottom, products, sums, records, and the guarded Kernel algorithm. Its type grammar and contexts are It retains only S-Refl, S-Trans, S-Top, S-Var, and S-Arr, restricted to this grammar, and replaces S-AllK by the rule below. Its body premise is checked under the target bound $T_1$.

A closed decision input may have a nonempty bound context. Precisely, is closed when each $A_i$ mentions only earlier $X_j$, and is closed when every free variable of $S,T$ is declared in $\mathrm{\Gamma }$. This is the input class of theorem 8.29; it is not restricted to $\mathrm{\Gamma }=\cdot$.