Dependent Records and Primitive Projections

A nested $\mathrm{\Sigma }$-type stores dependent components, but the terms ${\mathsf{pr}}_1({\mathsf{pr}}_1(r))$ and ${\mathsf{pr}}_2(r)$ do not say which components they select. Reordering two independent components also changes those terms. A true-record calculus makes field labels part of the syntax. That convenience comes with precise design choices: which occurrence of a repeated label is visible, how a field is removed while searching, and whether a record is judgmentally equal to the record of its projections.

Pollack’s left-associating true records

We freeze Pollack’s 2002 left-associating rules. If $L$ is a record signature and $A$ is a type family over records $l:L$, then $⟨L,r:A⟩$ appends a visible field $r$. A value $⟨l,r=a⟩$ stores a prefix $l:L$ and a last component $a:A(l)$. Labels do not bind in terms, and later occurrences shadow earlier ones.

The rule names Rec-form and Rec-intro are local to this dependent true-record calculus. They are not the simply typed record rules tabulated earlier in appendix A; the term formers and dependency premises distinguish the two signatures.

There is deliberately no record-eta equation $$\begin{array}{}\text{(}notarule\text{)}& l\stackrel{?}{\equiv }⟨l|r,r=l.r⟩.\end{array}$$ Pollack’s displayed true-record rules do not contain it. Coquand, Pollack, and Takeyama later use generalized eta-expansion inside normalization, but state explicitly that object equality contains neither surjective pairing nor record field permutation. Eta expansion as an algorithmic device must not be confused with judgmental record eta.

For a concrete dependency, start from $\mathbf{1}$ and form The notation in a later field type abbreviates the corresponding projections from the prefix variable. The closed value $$p:=⟨⟨⟨\star ,\mathsf{Carrier}=\mathbb{N}⟩,\mathsf{point}=\mathsf{0}⟩,\mathsf{loop}={\mathsf{refl}}_{\mathsf{0}}⟩:{\mathsf{PointedLoop}}_i$$ calculates by right-to-left lookup: The last two lines include passing steps. The loop field is checked only after the carrier and point fields have been substituted into its type.

Substitution and the Sigma comparison

The operation $l|r$ is what keeps the dependency well typed during field search. Substitution therefore acts simultaneously on the prefix, the field family, and every recursively exposed restriction.

Proof of Lemma 79.2 — Record substitution

Proof. Induct on the derivation. Formation and construction use ordinary substitution for $L$ and for the dependent field type $A(l)$. In Rec-proj, the induction hypothesis gives $l[u/x]:⟨L[u/x],r:A[u/x]⟩$; applying Rec-rest first gives the substituted prefix and then Rec-proj gives $$l[u/x].r:A[u/x][(l[u/x]|r)/z].$$ Capture-avoiding substitution composition identifies this classifier with $(A[l|r/z])[u/x]$. For Rec-rest-pass, the induction hypothesis supplies the substituted outer record and the recursive premise $((l|r)|p)[u/x]:P[u/x]$. Preserving $r\ne p$ reconstructs the conclusion $(l|p)[u/x]:P[u/x]$. For Rec-proj-pass, the recursive premise is $((l|r).p)[u/x]:P[u/x]$ and the reconstructed conclusion is $(l.p)[u/x]:P[u/x]$. For each of the four computation axioms, the induction hypotheses type the substituted operands and the same computation axiom, with all operands substituted, yields the required equality. A congruence case applies the induction hypothesis to every displayed premise and then rebuilds that same congruence rule; conversion uses the substituted type equality. These are all new cases. ◻

For pairwise fresh labels, flatten $⟨\cdots ⟨\mathbf{1},{\ell }_1:A_1⟩\cdots ,{\ell }_k:A_k⟩$ as $({\ell }_1:A_1,\dots ,{\ell }_k:A_k)$. Define a translation to prefix-nested Sigma types by Passing through a different top label first applies ${\mathsf{pr}}_1$ and continues recursively. Thus named selection becomes a finite projection spine.

Proof of Theorem 79.3 — The exact Sigma comparison

Proof. Induct on the record signature. At the last field, restriction beta translates to ${\mathsf{pr}}_1(l^S,a^S)\equiv l^S$, and projection beta to ${\mathsf{pr}}_2(l^S,a^S)\equiv a^S$. A passing computation translates to one outer first projection followed by the induction hypothesis. Formation and construction are Sigma formation and introduction. Congruence and conversion commute with the translation. Translating a derivation of a record-free conclusion leaves that conclusion unchanged, which proves conservativity. No converse eta step is used. ◻

Pollack compares left-associating records with labeled Sigma types at exactly this strength: restriction exposes the prefix and projection exposes the selected component. Repeated labels remain meaningful in his calculus, but the fresh-label fragment is the one used for the algorithmic correspondence below.

The record-only CPT correspondence

Coquand, Pollack, and Takeyama use right-associating records. We isolate the fragment ${\mathsf{CPT}}_{\mathsf{rec}}$ containing the empty signature $1$, signature extension $⟨\ell :A,x.B⟩$, empty value $()$, value extension $(\ell =M,N)$, and primitive selection $M.\ell$. Labels are fresh in a tail. Its two dot reductions are We exclude singleton and manifest fields, structural subtyping, signature strengthening, modules, and type-family application.

For a fresh-label Pollack signature $\mathrm{\Delta }=({\ell }_1:A_1,\dots ,{\ell }_k:A_k)$, define Pollack restriction is used only by the source lookup derivation; a maximal projection $q.\ell$ translates directly to CPT dot selection. Call this the projection fragment: restriction is not exposed as a standalone result term. This boundary is necessary because CPT’s record object syntax has dot selection but no whole-tail projection.

Proof of Theorem 79.4 — Pollack-to-CPT correspondence

Proof. For preservation, induct on the Pollack derivation. Formation and construction reverse the left-associated prefix into a right-associated CPT tail. A source projection search through $m$ later labels becomes exactly $m$ applications of the second rule in (79.4), followed by the first. Dependency is preserved because both derivations substitute the same earlier field values before checking a later type.

For reflection, invert the CPT derivation on the image grammar. A translated signature has a unique right-associated field spine and translated terms have only image constructors. Reconstruct Pollack formation or construction one field at a time. A dot derivation determines a unique label position because labels are fresh; rebuild the corresponding finite restriction search. The same induction reflects a dot-conversion chain to (79.1)–(79.3). No CPT subtyping or singleton rule occurs in the restricted derivation, so there is no remaining case. ◻

Proof of Theorem 79.5 — Checking and available canonicity for records

Proof. Use the correspondence theorem. The CPT normalizer extends neutral eta-expansion by the clauses printed with the record fragment; alpha-comparison of the resulting normal forms decides equality. Checking a constructor proceeds from the first field to the last, substituting each checked value into the remaining tail. Projection follows the unique finite label spine. Reflection transfers each successful or failed query back to the Pollack fragment.

For preservation, the selected dot redex $(\ell =M,N).\ell$ has the field type assigned to $M$. In the different-label case the typing derivation for $N.k$ is already a premise. The substitution lemma handles compatible reductions below dependent tails.

For canonicity, normalize the translated closed term. A closed neutral cannot be headed by a variable, and a dot-headed neutral would have a smaller closed neutral record scrutinee. Finite descent rules this out. Hence the normal form is $()$ at the empty signature or $(\ell =M,N)$ at an extension. Induction on the signature and the assumed base canonical forms gives the claim; reflection returns the corresponding left-associated Pollack value. Generalized eta-expansion helps the equality algorithm compare neutrals, but is nowhere oriented as a source reduction or asserted as source equality. ◻

Suggested first pass.

Begin with exercise 79.5, then complete exercise 79.6.

Exercise 79.5¶

★★☆ Extend ${\mathsf{PointedLoop}}_i$ by a Boolean name field. Give its left-associated Pollack signature, its right-associated CPT translation, and the complete dot-reduction trace for selecting the point and carrier fields. Mark the source restriction step corresponding to each target dot-pass step.

Referenced from 4 locations

• Dependent Records and Primitive Projections
• ch:dependent-records: ch:dependent-records

Exercise 79.6¶

★★★ Practical project.dependent-record-checker Implement in Kappa formation and checking for the fresh-label fragment of definition 79.1. Check fields from left to right and implement named projection by a right-to-left label search. Accept the displayed ${\mathsf{PointedLoop}}_i$ value and compute its point projection to zero. Reject a record whose carrier is $\mathbb{N}$, point is $\mathsf{0}$, and loop endpoints are both $\mathsf{suc}(\mathsf{0})$; name the expected and actual endpoint types. Also reject a duplicate-label declaration in this executable fragment. The acceptance test compares these exact results. This finite checker does not implement Pollack’s full repeated-label calculus or prove the correspondence theorem.

Referenced from 5 locations

• Dependent Records and Primitive Projections
• Object calculus checker and evaluator
• ch:dependent-records: ch:dependent-records