ch:polymorphic-record-compilation: ch:polymorphic-record-compilation

For $a::\mathsf{U}$, the image $\mathsf{String}$ is a well-formed type. For $r::\{\{\mathsf{Name}:a\}\}$, substitution produces the obligation $$\varnothing ⊢\{\mathsf{Age}:\mathsf{Nat},\mathsf{Name}:\mathsf{String}\}::\{\{\mathsf{Name}:\mathsf{String}\}\}.$$ Its finite-map inclusion premise holds because the concrete type contains the required field with exactly the substituted type. Thus the pair respects both bindings of $\mathcal{K}$, and K-Rec derives the displayed judgment.

The first label set sorts as $[\mathsf{Name},\mathsf{Office}]$, so $\mathsf{Name}$ has position $1$. The second sorts as $[\mathsf{Age},\mathsf{Name},\mathsf{Phone}]$, so it has position $2$. Therefore the two record values compile to and . Rule V-Nth types the selections at $\mathsf{String}$, and the two target roots are

After the two type applications, the selector has target term ${\lambda }^{\mathsf{i}}I.\lambda x:{\tau }_{\mathsf{H}}^{\ast }.x⟨I⟩$ and index-arrow result $\mathsf{idx}(\mathsf{Name},{\tau }_{\mathsf{H}}^{\ast }){\Rightarrow }_{\mathsf{i}}({\tau }_{\mathsf{H}}^{\ast }\to \mathsf{String})$, where ${\tau }_{\mathsf{H}}$ is the displayed concrete record type. In its translated layout, $\mathsf{Name}$ has position $2$, so IV-Pos derives $\varnothing ;\varnothing {⊢}_{\mathsf{V}}^{\mathsf{i}}2:\mathsf{idx}(\mathsf{Name},{\tau }_{\mathsf{H}}^{\ast })$. Rule V-IApp therefore derives $({\lambda }^{\mathsf{i}}I.\lambda x:{\tau }_{\mathsf{H}}^{\ast }.x⟨I⟩)@2:{\tau }_{\mathsf{H}}^{\ast }\to \mathsf{String}$. Rule V-Vec assigns the vector the type ${\tau }_{\mathsf{H}}^{\ast }$; target application gives type $\mathsf{String}$. The two target contractions yield .

The two source roots are Write $v_{\mathsf{J}}$ and $v_{\mathsf{H}}$ for the two source record values in the displayed roots, put and , and let ${\tau }_{\mathsf{J}}$ and ${\tau }_{\mathsf{H}}$ be their respective record types. The record clause gives the two exact membership judgments $$(v_{\mathsf{J}},A_{\mathsf{J}})\in {\mathcal{R}}_{\mathsf{rec}}^{{\tau }_{\mathsf{J}}},(v_{\mathsf{H}},A_{\mathsf{H}})\in {\mathcal{R}}_{\mathsf{rec}}^{{\tau }_{\mathsf{H}}}.$$ The canonical positions are $1$ and $2$, so the target roots are The base clause relates each resulting string constant to itself, which is the projection case of the fundamental relation for both records.

The translated type is The term inserts index abstractions in canonical label order: $$\mathrm{\Lambda }a.\mathrm{\Lambda }r.{\lambda }^{\mathsf{i}}{I}_{r,\mathsf{Age}}.{\lambda }^{\mathsf{i}}{I}_{r,\mathsf{Name}}.\lambda x.[x⟨I_{r,\mathsf{Age}}⟩,x⟨I_{r,\mathsf{Name}}⟩].$$ At the stated concrete type, the canonical layout is $[\mathsf{Age},\mathsf{Name},\mathsf{Phone}]$, so the supplied indices are $1,2$. The body is $[x⟨1⟩,x⟨2⟩]$, whose result layout is $[\mathsf{Age},\mathsf{Name}]$.

For the record-kinded abstraction case, fix $k=\{\{{\ell }_i:{\tau }_i\}{\}}_{i=1}^m$ in canonical order. The induction hypothesis is $${\mathcal{K}}^{\ast },t::k^{\ast };({\mathcal{L}}_{\mathcal{K}}{)}^{\ast },({\mathcal{L}}_{\mathcal{K},t}{)}^{\ast };{\mathcal{T}}^{\ast }{⊢}_{\mathsf{V}}C:{\sigma }^{\ast }.$$ Every variable in ${\mathcal{L}}_{\mathcal{K},t}$ has the form $I_{t,{\ell }_i}$. Every variable in ${\mathcal{L}}_{\mathcal{K}}$ has the form $I_{u,\ell }$ with $u\in \mathrm{dom}(\mathcal{K})$. Freshness of $t$ and global injectivity therefore make the domains disjoint. Applying V-IAbs for $i=m,m-1,\dots ,1$ derives the index-arrow suffix, and V-TAbs derives the translated universal.

For type application, canonical translation gives ${\mathcal{K}}^{\ast }{⊢}_{\mathsf{V}}{\tau }^{\ast }::k^{\ast }$. Index availability certifies $({\ell }_i,\tau )$ for $J_i$ in the source index judgment; clause 3 of lemma 8.13 gives, for every $i$, $${\mathcal{K}}^{\ast };({\mathcal{L}}_{\mathcal{K}}{)}^{\ast }{⊢}_{\mathsf{V}}^{\mathsf{i}}{J}_i:\mathsf{idx}({\ell }_i,{\tau }^{\ast }).$$ Rule V-TApp first derives $C[{\tau }^{\ast }]$; applying V-IApp in the canonical order derives the type ${\sigma }^{\ast }[{\tau }^{\ast }/t]$. By lemma 8.13, this type is $(\sigma [\tau /t]{)}^{\ast }$, which is the required conclusion.

Erasure leaves one target body $\lambda x.x⟨i⟩$. In the first opening layout the name is at $i=1$; in the second it is at $i=2$. Since $1\ne 2$, no numeral makes both calls select the name. Searching the vector for a run-time label can choose the right component, but the target operation is then a dynamic search rather than the constant numeric selection required by the compiler specification.

Use the record types $${\tau }_1=\{\mathsf{Name}:\mathsf{String},\mathsf{Office}:\mathsf{Nat}\},{\tau }_2=\{\mathsf{Age}:\mathsf{Nat},\mathsf{Name}:\mathsf{String}\}.$$ Both have exactly two distinct labels, so $|\mathrm{layout}({\tau }_1)|=2=|\mathrm{layout}({\tau }_2)|$. Their layouts are $[\mathsf{Name},\mathsf{Office}]$ and $[\mathsf{Age},\mathsf{Name}]$, and their name positions are $1$ and $2$. An unlabeled vector of length two does not reveal which layout produced it, so length and vector shape cannot determine the source projection. Passing the singleton-typed index $I:\mathsf{idx}(\mathsf{Name},r)$, instantiated to the concrete position at type application, restores exactly the missing information.