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

Problem and result. Compile finite source terms to a separate target AST. Records become canonical vectors, projections become certified one-based selections, and a record-kinded type abstraction becomes a type abstraction containing index binders. Type application must emit index-application syntax before a separate evaluator executes it. Reject missing fields and duplicate labels before target execution.

Representation. Use the following typed representation signatures:

Type   = TypeVar Name | TypeConst Name | RecordType Layout
Kind   = UniversalKind | RequiredFields Layout
Index  = IndexVar Name | IndexNat Nat
Source = SVar Name | SLam Name Type Source
       | SRecord [Field]
       | SProject Source Label
       | STypeAbs Name Kind Source
       | STypeApp Source Type Kind
Target = TVar Name | TLam Name Type Target
       | TVector [Value]
       | TSelect Target Index
       | TTypeAbs Name Kind Target | TTypeApp Target Type
       | TIndexAbs Name Target | TIndexApp Target Index
IndexBinding =
  { owner : Name, label : Label,
    variable : Name }
Result = Compiled Target | Rejected Reason

Keep source fields in their written order and layouts in sorted order. This makes the permutation inspectable. Key every index binding by the pair $(t,\ell )$ and extend the ambient binding list at a nested type abstraction. For binders $r$ and $s$ that both require $\mathsf{Name}$, extend $$[(r,\mathsf{Name},I_{r,\mathsf{Name}})]\text{to}[(s,\mathsf{Name},I_{s,\mathsf{Name}}),(r,\mathsf{Name},I_{r,\mathsf{Name}})].$$ A map keyed only by $\mathsf{Name}$ overwrites the outer binding. A single datatype mixing source projections with target selections would shorten the code, but it could not test that compilation emitted the target constructors.

First complete version. Implement label equality, decidable comparison, insertion sort, distinctness, field lookup, and one-based position lookup. The first complete pipeline is

compile(SProject(SRecord joe, Name)) =
  TSelect(TVector [Joe,403], IndexNat 1)
evaluate(TSelect(TVector [Joe,403], IndexNat 1)) = Joe

Compilation first validates distinct labels, sorts $[\mathsf{Office},\mathsf{Name}]$, constructs the vector, and emits the selection node. Evaluation begins only after the complete target term exists. This version is already end-to-end and has the observable result Joe.

Remaining cases. Compile Hanako’s record by the same C-Record and C-Dot order. Then add the proof-relevant cases in the order of the preservation argument. For C-TAbsRec, compile

STypeAbs "a" UniversalKind
  (STypeAbs "r" (RequiredFields [Name])
    (SLam "x" (TypeVar "r")
      (SProject (SVar "x") Name)))

to

TTypeAbs "a" UniversalKind
  (TTypeAbs "r" (RequiredFields [Name])
    (TIndexAbs "I_r_Name"
      (TLam "x" (TypeVar "r")
        (TSelect (TVar "x") (IndexVar "I_r_Name")))))

For C-TAppRec, carry the expected kind in the typed application node, validate the actual record type, compute the required position, and wrap the compiled term in TTypeApp and TIndexApp. The compiler can therefore translate the complete variable-headed input

STypeApp
  (SVar "f")
  (RecordType [Name,Office])
  (RequiredFields [Name])

to

TIndexApp
  (TTypeApp (TVar "f") (RecordType [Name,Office]))
  (IndexNat 1)

This compilation never inspects the operator for a syntactic STypeAbs. Pretty-print the AST to check $@1$ and $@2$ before calling the evaluator. Compile the nested source term

STypeAbs "r" (RequiredFields [Name])
  (SLam "x" (TypeVar "r")
    (STypeAbs "s" (RequiredFields [Age])
      (SProject (SVar "x") Name)))

and require its projection to use I_r_Name. Replace the inner [Age] by [Name]; the emitted names I_r_Name and I_s_Name must remain distinct. Add the missing-Phone and duplicate-Name inputs last; both must return Rejected before any target evaluation.

A failing version. Apply mutant-accept-duplicate-label.patch to a disposable copy. It replaces the distinctness guard by True. The mutated file still passes kappa check, but the duplicate-label candidate reaches vector construction and changes the direct rejection oracle to FAIL. That candidate is SRecord [Name=Joe,Name=Hanako].

Acceptance test. Require both source field maps, both computed layouts, both target vectors, indices $1$ and $2$, both translated concrete selections, the full $\mathsf{U}$-then-record-kinded selector AST, computed $@1$ and $@2$ instantiation ASTs, and the separately evaluated values Joe and Hanako. Require the traces named nested-outer and nested-same-label, the variable-operator application, and both pre-execution rejections. The accepted run must end with the exact summary All 13 Chapter 8 corpus cases passed. and an empty audit. The check-clean mutant must fail its test oracle.

Mathematical boundary. The run exercises the constructor cases used by compiler totality and type preservation. It does not prove those theorems, the logical relation, or the full Ohori theorem.