ch:path-dependent-types: stable paths and pDOT

From $r:\mathsf{Root}$, DOT-Rec-E exposes $$r:\{palette:\mathsf{Palette}\}\wedge \{default:r.palette.Color\}.$$ The first intersection projection and DOT-Fld-E give $r.palette:\mathsf{Palette}$. Rule P-Var first gives $r\mathsf{path}$; the field typing just derived then gives $r.palette\mathsf{path}$ by P-Fld. Eliminating the recursive palette type exposes its member declaration $\{Color:\mathrm{\perp }..\mathrm{\top }\}$, so selection forms $r.palette.Color$. Finally the second root intersection projection gives $$r:\{default:r.palette.Color\}.$$ Rule DOT-Fld-E derives $$r.default:r.palette.Color.$$

Let The first Repl-$pq$ instance changes only the occurrence in the $a$-field, using $\mathrm{\Gamma }⊢\mathrm{Replace}(T_0,p,q,T_1)$, and derives . The second uses $\mathrm{\Gamma }⊢\mathrm{Replace}(T_1,p,q,T_2)$ for the $b$-field and derives . Transitivity gives . Each indexed replacement derivation ends in R-Sel, whose second premise forms the complete changed selection $\mathrm{\Gamma }⊢q.A\mathsf{type}$.

Extend the family by and replace $\mathsf{Tree}$ by ${\mathsf{Tree}}_{\mathsf{pal}}$ in the three declarations of $\mathrm{\Gamma }$. Recursion elimination at $\mathit{apple}$ supplies the exact field premise $$\mathrm{\Gamma }⊢\mathit{apple}:\{palette:\mathsf{Palette}\}.$$ Together with $\mathrm{\Gamma }⊢\mathit{apple}\mathsf{path}$, obtained by P-Var, this is the premise of P-Fld; hence $$\mathrm{\Gamma }⊢\mathit{apple}.palette\mathsf{path},\mathrm{\Gamma }⊢\mathit{apple}.palette.Color\mathsf{type}.$$ The corresponding two premises for orange are $$\mathrm{\Gamma }⊢\mathit{orange}\mathsf{path},\mathrm{\Gamma }⊢\mathit{orange}:\{palette:\mathsf{Palette}\}.$$ They yield the selected type $\mathit{orange}.palette.Color$.

Now use $\mathit{alias}:\mathit{orange}.\mathsf{type}$. The first Sngl-E, with the target path $\mathit{orange}.palette$, derives $$\mathrm{\Gamma }⊢\mathit{alias}.palette:(\mathit{orange}.palette).\mathsf{type}.$$ The second Sngl-E, with target path $\mathit{orange}.palette.zero$, derives $$\mathrm{\Gamma }⊢\mathit{alias}.palette.zero:(\mathit{orange}.palette.zero).\mathsf{type}.$$ Field typing gives $\mathit{alias}.palette.zero:\mathit{alias}.palette.Color$, while Sngl-Trans and $\mathit{orange}.palette.zero:\mathit{orange}.palette.Color$ give the same path the type $\mathit{orange}.palette.Color$.

Finally R-Sel constructs the one-occurrence replacement, and Repl-$pq$ gives the requested agreement direction Rule Repl-$qp$ gives the converse. Thus the two selected Color types agree by mutual subtyping. The apple selection remains unrelated, as it should for a distinct tree family.

The displayed store yields the lookup chain Rule Lookup-Path rewrites the pending $x.a.c$ lookup through the intermediate alias $y.b.c$, after which Lookup-Val supplies the last line. Precise field typing gives $x.a.c:\mathrm{\forall }(z:\mathrm{\top })\mathrm{\top }$. With $y:\mathrm{\top }$, dependent application therefore has type $\mathrm{\top }$. Ordinary term progress first encounters the normal path $x.a.c$; exactly there lemma 108.9 ensures that extended reduction reaches the displayed lambda, enabling the beta step with $y$.

$x$ is a stable path by P-Var; $x.a.b$ is a stable path after two P-Fld instances, provided both field typings exist. Application $(\lambda y.y)x$ is rejected because the path grammar has no application clause. The object value $\nu (x:T)d$ is rejected because it has no object- construction clause. The whole let expression is rejected because it has no let clause, even though its bound expression and the body path $y.b$ may separately be stable.

Install a root $r$ whose $palette$ field contains a tight member $Color:T..T$ and a value $zero:T$, whose $alias$ definition is the path $r.palette$, and whose $default$ definition is $r.alias.zero$. Def-Path gives $r.alias:r.palette.\mathsf{type}$. Since $r.palette.Color$ is formed, singleton propagation and one-occurrence replacement give the two tight comparisons Field typing gives $r.default:r.alias.Color$; subsumption along the first comparison yields $r.default:r.palette.Color$. The derivation transports the selected type along the stable alias and does not assert raw syntactic equality of the paths.

Take $$\mathrm{\Gamma }=q:\mathrm{\top },p:q.\mathsf{type}\wedge \{a:\{A:\mathrm{\perp }..\mathrm{\top }\}\}.$$ The intersection component forms $p.a.A$, and the singleton component gives $p:q.\mathsf{type}$. A root-only replacement would change that occurrence to $q.a.A$. Rule RP-Fld blocks it because P-Fld cannot derive $\mathrm{\Gamma }⊢q.a\mathsf{path}$ from $q:\mathrm{\top }$. Even if that premise were deleted, R-Sel would still require $\mathrm{\Gamma }⊢q.a.A\mathsf{type}$, which also has no derivation. Thus the indexed prefix and complete-leaf checks reject the malformed replacement.

Let the enclosing object have stable path $p$, and let its nested field be $$a=\nu (y:T)d.$$ The installed inner self is the stable path $p.a$. Inverting Def-New gives the body judgment $$p.a;\mathrm{\Gamma }⊢d[p.a/y]:T[p.a/y].$$ The tight-record premise supplies equal member bounds and pairwise distinct labels. Intrinsic well-formedness of the body derivation supplies the path-formation steps for every path in the two substituted expressions $$d[p.a/y]\text{and}T[p.a/y].$$ Rule Def-New has no separate path side condition. When the nested object is added to the store, extend the runtime context with $p.a:\mu (y:T)$ and with the precise field declarations obtained from $T[p.a/y]$. The body premise types the stored definitions at those declarations. Disjoint labels make field lookup unique. Hence the extended store matches the extended inert, well-formed context, and the surrounding installation term retains its type.