Type-Preserving Compilation of Polymorphic Records

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Fix a decidable total order on a countable set of labels. Its running segment is The selector $$\mathsf{name}=\lambda r.r.\mathsf{Name}$$ has one polymorphic record type. Applying it to the two records below needs different machine instructions. Write $M{⇝}_{\mathsf{rec}}C$ when source term $M$ compiles to target term $C$. If records are vectors ordered by label, then The first selection needs index $1$ and the second needs index $2$. Erasing the record type before choosing that number loses information; keeping a run-time label search loses constant-time selection. The type abstraction must therefore also abstract over the index required for that field.

Required fields do not determine a layout

Labels also have decidable equality. The order’s decision procedure returns, for any two labels, exactly one of less than, equal, or greater. Thus sorting a finite label list is an algorithm, not merely an existence argument. Base types are written $b$, source monotypes are written $\tau$, type variables are written $t,u$, and result types are written $\upsilon$. The book-defined source calculus has Labels in either displayed finite field map are distinct. Their written order has no semantic force.

The calculus isolates index passing. A term is Church-style here when it writes every type abstraction $\mathrm{\Lambda }t::k.M$ and every type application $M[\tau ]$ explicitly. The calculus omits polymorphic let, record modification, variants, and operation annotations. It is therefore a pedagogical simplification inspired by the record-compilation mechanism, not a literal syntactic fragment of Ohori’s source language.

For example, $$\mathcal{K}=\{a::\mathsf{U},r::\{\{\mathsf{Name}:a\}\}\}\text{gives}\mathcal{K}⊢r::\{\{\mathsf{Name}:a\}\}.$$ Both concrete record types from the opening satisfy the ground instance with $a=\mathsf{String}$.

Replacing a required-field map $F^{\prime }$ by a submap $F\subseteq F^{\prime }$ is a weakening of the record kind: it removes requirements without changing the complete record type.

Proof of Lemma 8.3 — Formation and record-kind weakening

Proof. For clause 1, invert the final kinding rule. Rule K-Type contains the required formation premise. Rule K-VarRec has subject $t$, and Ty-Var forms $t$. Rule K-Rec contains $\mathcal{K}⊢\tau ::\mathsf{U}$; inversion of K-Type gives formation.

For clause 2, invert the record-kinding derivation. In K-VarRec, the map assigned to the variable contains $F^{\prime }$ and therefore contains $F$, so a K-VarRec instance gives the result. In K-Rec, the complete record map contains $F^{\prime }$ and $F^{\prime }\supseteq F$; transitivity of finite-map inclusion supplies the premise of a K-Rec instance. ◻

Proof of Lemma 8.4 — Formation substitution

Proof. Induct on the formation derivation. The base case is unchanged. The arrow and record cases apply the induction hypotheses to their premises; record labels remain distinct because substitution changes only field types. In the variable case, respect gives ${\mathcal{K}}^{\prime }⊢S(t)::S(\mathcal{K}(t))$, and clause 1 of lemma 8.3 extracts the required formation judgment. ◻

Proof of Lemma 8.5 — Kinding substitution

Proof. Induct on the displayed kinding derivation. In K-Type, lemma 8.4 gives formation of $S(\tau )$, so a K-Type instance applies. In K-VarRec, respect gives ${\mathcal{K}}^{\prime }⊢S(t)::S(\mathcal{K}(t))$. The required field map is a submap of $S(\mathcal{K}(t))$, so clause 2 of lemma 8.3 gives the conclusion. In K-Rec, lemma 8.4 forms the substituted complete record. Substitution preserves labels and finite-map inclusion, so K-Rec applies. ◻

The explicitly typed source

The kinding judgment proves that projection is legal, but it does not yet connect the proof to a term. The source system is fixed here so that every later compiler case has exactly one typing rule to follow.

Source terms are Here $c^b$ is a constant whose base type is $b$. The record form is part of the raw syntax only when ${\ell }_1,\dots ,{\ell }_n$ are distinct. Thus a duplicate-label input is rejected before it becomes a source term. Terms are identified up to renaming of bound term and type variables. A type assignment $\mathcal{T}$ maps distinct term variables to source types formed under $\mathcal{K}$.

The polymorphic selector is now explicit: $$\mathsf{name}:=\mathrm{\Lambda }a::\mathsf{U}.\mathrm{\Lambda }r::\{\{\mathsf{Name}:a\}\}.\lambda x:r.x.\mathsf{Name}.$$ Its complete type is $$\mathrm{\forall }a::\mathsf{U}.\mathrm{\forall }r::\{\{\mathsf{Name}:a\}\}.r\to a.$$ The premise of R-Dot is supplied by K-VarRec; the two uses of R-TAbs then close the derivation.

If type arguments are erased before layout selection, both calls to $\mathsf{name}$ become the same target function but demand different numeric indices. This is the obstruction that forces index passing.

A target with vectors and index abstraction

For a concrete record type $\tau$, let $\mathrm{layout}(\tau )$ be its labels sorted by . If $\ell$ occurs in that list, then ${\mathrm{pos}}_{\ell }(\tau )$ is its one-based position. The operation is undefined on an abstract type variable. This chapter’s target uses one-based positions; the array target in chapter 4 uses zero-based offsets. Thus the first component has position $1$ here.

Index expressions are $J::=i\mid I$, where $i$ is a positive numeral and $I$ is an index variable.

Their source certification judgment is $\mathcal{K};\mathcal{L}{⊢}_{\mathsf{R}}^{\mathsf{i}}J\mathsf{certifies}(\ell ,\tau )$, with rules

$\mathcal{L}(I)=(\ell ,\tau )$

$\mathcal{K};\mathcal{L}{⊢}_{\mathsf{R}}^{\mathsf{i}}I\mathsf{certifies}(\ell ,\tau )$

$\mathcal{K}⊢\tau ::\{\{\ell :\upsilon \}\}$$i={\mathrm{pos}}_{\ell }(\tau )$

$\mathcal{K};\mathcal{L}{⊢}_{\mathsf{R}}^{\mathsf{i}}i\mathsf{certifies}(\ell ,\tau )$

The target judgment $\mathcal{H};\mathcal{I}{⊢}_{\mathsf{V}}^{\mathsf{i}}J:\mathsf{idx}(\ell ,\rho )$ is generated by the parallel rules

$\mathcal{I}(I)=\mathsf{idx}(\ell ,\rho )$

$\mathcal{H};\mathcal{I}{⊢}_{\mathsf{V}}^{\mathsf{i}}I:\mathsf{idx}(\ell ,\rho )$

$\mathcal{H}{⊢}_{\mathsf{V}}\rho ::\{\{\ell :{\rho }^{\prime }\}\}$$i={\mathrm{pos}}_{\ell }(\rho )$

$\mathcal{H};\mathcal{I}{⊢}_{\mathsf{V}}^{\mathsf{i}}i:\mathsf{idx}(\ell ,\rho )$

Proof of Lemma 8.10 — Totality and typing of numeral substitution

Proof. Every binding has the form $I_{t,\ell }:\mathsf{idx}(\ell ,t)$ for a field required by $\mathcal{K}(t)$. Because $S$ respects $\mathcal{K}$, rule K-Rec or K-VarRec shows that $S(t)$ contains the $\ell$ field. Decidable sorting gives its unique positive position. Rule IV-Pos derives the displayed judgment. ◻

The central layout bookkeeping can be read in three columns. A row begins with a source label, points to its slot in the canonical target vector, and ends with the numeral inhabiting the corresponding index type:

Here ${\tau }_{\mathsf{J}}$ and ${\tau }_{\mathsf{H}}$ are the two concrete opening record types. Every row asserts the invariant $i={\mathrm{pos}}_{\ell }(\tau )$; the table illustrates that invariant and does not replace its proof.

Target terms are generated by Angle brackets distinguish vector selection $C⟨J⟩$ from type application $C[\rho ]$.

The semantic theorem needs the exact compatible closure, not only the two target-specific roots. Source values and target values are The source evaluation contexts $E_{\mathsf{R}}$ and target evaluation contexts $E_{\mathsf{V}}$ evaluate applications and aggregate components from left to right: The comma-separated record-context line denotes the record whose fields before $i$ are values, whose $i$th field is the hole, and whose later fields are unevaluated. The root contractions are and The relations ${⟶}_{\mathsf{R}}$ and ${⟶}_{\mathsf{V}}$ are the compatible closures under their respective contexts. Their reflexive–transitive closures are ${{⟶}^{\ast }}_{\mathsf{R}}$ and ${{⟶}^{\ast }}_{\mathsf{V}}$. Write $M{\Downarrow }_{\mathsf{R}}v$ when $M{{⟶}^{\ast }}_{\mathsf{R}}v$, and write $M{\Uparrow }_{\mathsf{R}}$ when there is an infinite ${⟶}_{\mathsf{R}}$ sequence from $M$; use the corresponding $\mathsf{V}$ notation for target terms.

Proof of Lemma 8.12 — Determinism and evaluation-prefix closure

Proof. Each nonvalue has at most one decomposition into a displayed evaluation context and a displayed root redex: application and aggregate contexts choose the leftmost nonvalue, while type application, projection, selection, and index application evaluate only their operator. The raw-syntax distinctness condition gives exactly one field with the projected label, and a numeric vector position names exactly one component. Every root therefore has one contractum, so both step relations are deterministic.

For prefix closure, a finite prefix cannot change whether a deterministic sequence is infinite. If evaluation terminates, deleting or adding a finite prefix preserves its unique terminal value. Hence the two terms diverge together before the prefixes exactly when they do afterward, and their terminal pair belongs to $W$ before the prefixes exactly when it does afterward. ◻

Type-directed index passing

The translation of a quantified type records the index arguments required by its kind. Before translating a record kind, enumerate its finite field map in increasing label order; hence the indices $1,\dots ,m$ below are canonical and do not depend on the source presentation order. Write $k=\{\{{\ell }_i:{\tau }_i\}{\}}_{i=1}^m$ and $k^{\ast }=\{\{{\ell }_i:{\tau }_i^{\ast }\}{\}}_{i=1}^m$. Define In the record-type line, the superscript star applies to the whole type on the left; labels are not translated. Translation acts pointwise on contexts: Thus ${\mathcal{K}}^{\ast }$ is a target kind assignment, ${\mathcal{T}}^{\ast }$ is a target term assignment, and ${\mathcal{L}}^{\ast }$ is a target index assignment.

Proof of Lemma 8.13 — Canonical translation and index transport

Proof. Prove clauses 1 and 2 simultaneously by induction on source formation and kinding. Base and variable translations are identities. Arrow premises use the two formation induction hypotheses. In a record premise, decidable sorting changes neither labels nor their associated translated field types, so it preserves formation and finite-map inclusion. These are exactly the target instances of Ty-Rec, K-VarRec, and K-Rec.

For clause 3, invert the source index judgment. Rule IR-Var becomes IV-Var by the pointwise definition of ${\mathcal{L}}^{\ast }$. Rule IR-Pos uses clause 2; translation preserves the label set and hence the sorted position, so IV-Pos applies with the same numeral.

The substitution equation follows by induction on $\sigma$. At a record type, substitution changes field types but not labels, so both sides use the same sorting permutation. The canonical-assignment equation follows from the pairwise definition of $I_{t,\ell }$, and the free-variable equation follows by induction on every type in $\mathcal{T}$. Finally, induction on the ordered bindings of $\mathcal{K}$ uses clause 1 on every field type of the translated kind and then applies VK-U or VK-Rec. ◻

By C-TAbsU, C-TAbsRec, C-Lam, and C-Dot, the selector of equation 8.2 compiles to $$\mathrm{\Lambda }a::\mathsf{U}.\mathrm{\Lambda }r::\{\{\mathsf{Name}:a\}\}.{\lambda }^{\mathsf{i}}{I}_{r,\mathsf{Name}}.\lambda x:r.x⟨I_{r,\mathsf{Name}}⟩.$$ The two ground instantiations of equation 8.9 pass $1$ and $2$, respectively. After those index applications, every field access is the constant-time vector operation in V-Nth; no labels remain in the selection instruction.

Proof of Lemma 8.15 — Index availability

Proof. Invert the kinding derivation. If it ends in K-Rec, the finite-map inclusion places $\ell$ in the concrete record type. Sorting distinct labels gives one position, so the numeric index judgment holds. If it ends in K-VarRec, the kind assignment for $t$ contains the field. Equation 8.3 places exactly one corresponding binding in ${\mathcal{L}}_{\mathcal{K}}$. ◻

Proof of Theorem 8.16 — Total and deterministic compilation

Proof. Induct on the displayed source typing derivation. Rules R-Var and R-Const determine C-Var and C-Const. The induction hypothesis for the body of R-Lam determines its target body; C-Lam then determines the target annotation. The two induction hypotheses for R-App determine both target subterms, so C-App determines their application.

For R-Record, apply the induction hypothesis to every field. Decidable comparison computes one sorting permutation of the distinct labels, so C-Record exists and no second target vector order is possible. For R-Dot, lemma 8.15 gives exactly one $J$; C-Dot therefore exists and is determined.

For R-TAbs at a record kind, the pair-index allocator gives the unique extension ${\mathcal{L}}_{\mathcal{K},t}$. It is disjoint from ${\mathcal{L}}_{\mathcal{K}}$ because $t$ is fresh. The induction hypothesis determines the body, and C-TAbsRec inserts the index binders in canonical label order. Renaming those binders accounts for the stated alpha-equivalence. At kind $\mathsf{U}$, C-TAbsU adds no index binder. For R-TApp, lemma 8.15 determines each required actual index; C-TAppRec or C-TAppU then determines the target. These are all source rules. ◻

Proof of Theorem 8.17 — Type preservation of record compilation

Proof. Induct simultaneously on the source typing derivation and the matching compilation derivation. At each premise, translate all three assignments by equation 8.8; this is necessary because record types in kind, index, and term assignments are canonically reordered.

Variable and constant. Translation of the type assignment gives the target variable rule, and base constants retain their base type.

Term abstraction. The induction hypothesis under $\mathcal{T},x:{\tau }_1$ gives $C:{\tau }_2^{\ast }$ under ${\mathcal{T}}^{\ast },x:{\tau }_1^{\ast }$. Target abstraction derives $\lambda x:{\tau }_1^{\ast }.C:{\tau }_1^{\ast }\to {\tau }_2^{\ast }$.

Application. The two induction hypotheses give $C_1:{\tau }_1^{\ast }\to {\tau }_2^{\ast }$ and $C_2:{\tau }_1^{\ast }$. Target application gives $C_1{C}_2:{\tau }_2^{\ast }$.

Record. For every field, the induction hypothesis gives $C_i:{\tau }_i^{\ast }$. The rule C-Record reorders the type entries by the same label permutation. Rule V-Vec therefore derives the canonically presented translated record type from equation 8.7.

Projection. The induction hypothesis gives $C:{\tau }^{\ast }$. Clause 2 of lemma 8.13 translates the kinding premise to ${\mathcal{K}}^{\ast }{⊢}_{\mathsf{V}}{\tau }^{\ast }::\{\{\ell :{\upsilon }^{\ast }\}\}$. The compilation premise certifies $(\ell ,\tau )$ for $J$ in the source index judgment; clause 3 transports it to ${\mathcal{K}}^{\ast };({\mathcal{L}}_{\mathcal{K}}{)}^{\ast }{⊢}_{\mathsf{V}}^{\mathsf{i}}J:\mathsf{idx}(\ell ,{\tau }^{\ast })$. Rule V-Nth yields $C⟨J⟩:{\upsilon }^{\ast }$.

Type abstraction. First consider the record kind $k=\{\{{\ell }_i:{\tau }_i\}{\}}_{i=1}^m$. The induction hypothesis under $\mathcal{K},t::k$ has target kind assignment ${\mathcal{K}}^{\ast },t::k^{\ast }$. The disjoint source extension translates as $$({\mathcal{L}}_{\mathcal{K},t}{)}^{\ast }=\{I_{t,{\ell }_i}:\mathsf{idx}({\ell }_i,t)\mid 1\le i\le m\}.$$ Thus the induction hypothesis uses the two disjoint target assignments $$({\mathcal{L}}_{\mathcal{K}}{)}^{\ast },({\mathcal{L}}_{\mathcal{K},t}{)}^{\ast }.$$ Repeated V-IAbs removes this disjoint suffix and derives the index-arrow body of equation 8.7. Since $t$ is fresh for $\mathcal{K}$ and the source premise has $t\notin \mathrm{ftv}(\mathcal{T})$, clause 4 of lemma 8.13 gives $t\notin \mathrm{ftv}(({\mathcal{L}}_{\mathcal{K}}{)}^{\ast },{\mathcal{T}}^{\ast })$. Rule V-TAbs therefore derives the outer $\mathrm{\forall }t::k^{\ast }$. For $k=\mathsf{U}$, freshness of $t$ for $\mathcal{K}$ together with the source freshness premise for $\mathcal{T}$ gives the two target freshness conditions, so V-TAbs applies directly.

Type application. The induction hypothesis gives the translated universal type. Clause 2 of lemma 8.13 gives ${\mathcal{K}}^{\ast }{⊢}_{\mathsf{V}}{\tau }^{\ast }::k^{\ast }$, so V-TApp derives the translated universal body. For every record-kind field, the matching compilation premise certifies $({\ell }_i,\tau )$ for $J_i$ in the source index judgment. Clause 3 transports it to $J_i:\mathsf{idx}({\ell }_i,{\tau }^{\ast })$ in the target index judgment. Applying V-IApp $m$ times gives ${\sigma }^{\ast }[{\tau }^{\ast }/t]$, equal to $(\sigma [\tau /t]{)}^{\ast }$ by structural induction on $\sigma$. No index applications occur for $\mathsf{U}$.

These cases cover every source typing rule. ◻

The logical relation follows the representation

Type preservation says where compiled terms live. It does not yet say that vector position $2$ denotes the source field named $\mathsf{Name}$. Define a relation that follows the canonical layout.

For the outer selector binder, choose $S(a)=\mathsf{String}$. The inner binder kind is interpreted as $S(\{\{\mathsf{Name}:a\}\})=\{\{\mathsf{Name}:\mathsf{String}\}\}$. Thus both opening record types are well-scoped choices for $r$; the type environment carries the ground type that a relation-only environment loses.

Let $v_{\mathsf{J}},A_{\mathsf{J}}$ and $v_{\mathsf{H}},A_{\mathsf{H}}$ be the two source-record/target-vector pairs in the opening calculation, and let ${\tau }_{\mathsf{J}},{\tau }_{\mathsf{H}}$ be their record types. The record clause computes to $$(v_{\mathsf{J}},A_{\mathsf{J}})\in {\mathcal{V}}_{\mathsf{rec}}^{\varnothing ,\varnothing }({\tau }_{\mathsf{J}}),(v_{\mathsf{H}},A_{\mathsf{H}})\in {\mathcal{V}}_{\mathsf{rec}}^{\varnothing ,\varnothing }({\tau }_{\mathsf{H}}).$$ The pair with target is not in the first relation: its first component would have to relate the source $\mathsf{Name}$ string to the target office numeral. This near-nonexample tests the canonical permutation clause.

Proof of Lemma 8.19 — Closing and compatibility

Proof. The two equalities follow by induction on $\sigma$. The variable case is the definition of ${\chi }_S$. In the universal case, both sides quantify over $\varnothing ⊢\tau ::S(k)$ and extend by the same closed type and the same closed value relation.

For clause 1, split on the term relation for the function and then for the argument. Matched divergence makes both call-by-value applications diverge. Matched termination gives an arrow-related pair of function values and a value-related argument pair; the arrow clause gives the result, and lemma 8.12 adds the evaluation prefixes.

For clause 2, first suppose every related field pair terminates. The source record reaches its field values in written order, while the target vector reaches the related target values in canonical label order. The two orders may differ, but both evaluations are finite; after both finish, equation 8.11 relates the resulting aggregates. Otherwise, let ${\ell }_p$ label the first divergent source field in presentation order, and let ${\ell }_q$ label the first divergent target component in canonical order. Fieldwise relatedness makes the set of divergent labels the same on both sides. Every source field preceding the occurrence labelled ${\ell }_p$ terminates, as does every target component preceding the occurrence labelled ${\ell }_q$. The two aggregates therefore take possibly different finite prefixes and then both diverge. This proves clause 2 without claiming that source and target visit fields in the same order.

For clause 3, matched divergence is preserved by the projection contexts. In the terminating case, equation 8.11 places the $\ell$ components at the source field and canonical target position; the two roots in equation 8.5, equation 8.6 return those components. Clause 4 is exactly equation 8.12, followed by evaluation-prefix closure. ◻

Proof of Lemma 8.20 — Closing substitution equality

Proof. Induct on $\sigma$. The variable case distinguishes $t$ from the variables in $\mathrm{dom}(S)$; the remaining constructors apply the induction hypotheses to their immediate type components. ◻

Proof of Theorem 8.21 — Fundamental compilation relation

Proof. Induct simultaneously on the source typing derivation and the matching compilation derivation, keeping $S,\eta ,\zeta$ arbitrary. The decisive invariant is that $S$ closes kinds while the separate ${\nu }_S$ closes index variables.

Variable and constant. The environment hypothesis is exactly the variable conclusion. A base constant compiles to itself, so the base clause applies.

Term abstraction. Take any $(a,A)\in {\mathcal{V}}_{\mathsf{rec}}^{S,{\chi }_S}({\tau }_1)$. Extend $\eta$ by $x\mapsto a$ and $\zeta$ by $x\mapsto A$. The induction hypothesis for the body gives the term relation at ${\tau }_2$. The two term-beta roots and lemma 8.12 establish the arrow clause.

Application. The two induction hypotheses give the function and argument term relations. Clause 1 of lemma 8.19 gives the application relation.

Record. Each field induction hypothesis gives the corresponding term relation. Clause 2 of lemma 8.19 builds the labeled record and the target vector in the permutation computed by C-Record.

Projection. The induction hypothesis gives the record term relation. If compilation chose a concrete numeral, it is ${\mathrm{pos}}_{\ell }(S(\tau ))$. If it chose $I_{t,\ell }$, lemma 8.10 gives ${\nu }_S(I_{t,\ell })={\mathrm{pos}}_{\ell }(S(t))$. Clause 3 of lemma 8.19 therefore gives the projection result.

Type abstraction. Take a closed type $\tau$ with $\varnothing ⊢\tau ::S(k)$, and put $S^{\prime }=S[t\mapsto \tau ]$. Global injectivity gives the disjoint equation $${\nu }_{S^{\prime }}={\nu }_S,\{I_{t,{\ell }_i}\mapsto {\mathrm{pos}}_{{\ell }_i}(\tau ){\}}_{i=1}^m.$$ The induction hypothesis for the body under $S^{\prime }$ gives the relation after the source type-beta root, target type-beta root, and the $m$ index-beta roots. This proves equation 8.12; for $k=\mathsf{U}$, $m=0$.

Type application. The induction hypothesis for the polymorphic term gives the universal term relation. Put $\hat{\tau }=S(\tau )$ and $S^{\prime }=S[t\mapsto \hat{\tau }]$. Kinding substitution gives $\varnothing ⊢\hat{\tau }::S(k)$. Clause 4 of lemma 8.19 applies the target to the positions inserted by C-TAppRec; lemma 8.10 identifies each closed $J_i$ with that position. Its conclusion is indexed by $S^{\prime }$ and ${\chi }_{S^{\prime }}={\chi }_S[t\mapsto {\mathcal{V}}_{\mathsf{rec}}^{\varnothing ,\varnothing }(\hat{\tau })]$. The type-application case therefore reduces to the equality of term relations

The listed cases cover every source and compilation rule, so equation 8.13 follows. ◻

Proof of Corollary 8.22 — Semantic correctness at observable types

Proof. Apply theorem 8.21 with empty environments and the identity ground substitution. Induction on the observable type turns the clauses of ${\mathcal{R}}_{\mathsf{rec}}^{\sigma }$ into equality of base constants and the stated canonical record permutation. ◻

The theorem owned by the full Ohori calculus

The local calculus omitted let-generalization, record modification, and variants so that the index-passing proof could be followed without an inference algorithm. Ohori’s theorem applies to a larger, fixed signature.

Proof of Theorem 8.23 — Ohori's compilation theorem

Imported proof. The proof in Ohori’s appendix is a logical-relations induction. Its projection mechanism matches the local relation. Its additional cases cover modification, tag selection, switches, polymorphic let, vacuous type-variable elimination, and interacting index assignments. The imported theorem owns those cases. They are not consequences of the book-defined record-only proof. ◻

The source and target calculi, type translation, and general correctness signature are due to Ohori [Oho95]. The final seminar sequence is adapted to the representation calculations in the Régis-Gianas–Rémy examination [RGR11]; the implementation comparison uses the pinned program of [Uta19] only as executable corroboration.