Type-preserving compilation of polymorphic records

The local source is a book-defined Church-style simplification of Ohori’s mechanism: base types, arrows, kinded universals, finite fixed-label record types, record construction, and projection. Record kinds require finite distinct-field maps, and K-Rec checks whole-record formation. The target retains type abstraction and adds sorted vectors, one-based singleton index types, and explicit index abstraction/application. Both calculi have complete left-to-right call-by-value contexts and term-beta, type-beta, and representation-specific roots. The local source omits inference, Poly, polymorphic let, annotated operations, modification, and variants.

Kinding substitution, index availability, type translation canonicalization for monotypes, globally fresh allocation, numeral-substitution typing, compiler totality and determinism, type preservation, evaluation-prefix closure, the closing source-target logical relation, and observable correctness are proved by complete inductions in chapter 8. The logical relation carries both a closing type environment and its indexed value relations.

Ohori’s Theorem 4.5.1 has premise ${\mathrm{\Lambda }}^{\mathsf{let},\bullet }⊢K,T▹M:\sigma$ and $C(L_K,(T{)}^{\ast },M)=C$. For every ground $S$ respecting $K$ and every environment pair in $R^{S(T)}$, its conclusion relates ${\eta }_1(\mathrm{erase}M)$ and ${\eta }_{2,S(L_K)}(C)$ in $R^{S\sigma }$. No stronger target equivalence or inference theorem is imported.

The Kappa companion in artifacts/ch8-polymorphic-record-compiler/ has separate recursive source and target ASTs, typed lambda nodes, kinded type nodes, and pair-keyed index assignments. It computes and prints target vectors, concrete selections, the nested-outer and nested-same-label terms, type/index applications, and the two opening results; missing and duplicate fields are rejected before the separate evaluator runs. It is finite implementation evidence, not a mechanization of totality, preservation, or logical relatedness.