Fully Path-Dependent Types: Stable Paths, Singletons, and Modules

Proof. First prove that every derivation $\mathrm{\Gamma }⊢\mathrm{RPath}(r,p,q,r^{\prime })$ contains a derivation of $\mathrm{\Gamma }⊢q\mathsf{path}$. Induction on $\mathrm{RPath}$ has two cases. Rule RP-Here supplies the required premise. Rule RP-Fld preserves the induction hypothesis while adding formation of $r^{\prime }.a$.

Now induct on the displayed $\mathrm{Replace}$ derivation. The leaf rules R-Sel and R-Sngl contain an $\mathrm{RPath}$ premise, so the preceding induction gives $\mathrm{\Gamma }⊢q\mathsf{path}$. Every structural replacement rule has exactly one premise; applying the induction hypothesis to that premise retains the same target root $q$. Thus every case supplies $\mathrm{\Gamma }⊢q\mathsf{path}$. Apply Repl-$pq$ to that path judgment, the assumed alias, and the assumed replacement derivation. ◻

Proof. Induct on the indexed replacement derivation. In R-Sel and R-Sngl, the second premise is exactly the required formation derivation for the changed leaf. In R-Fld, inversion of source formation gives $\mathrm{\Gamma }⊢S\mathsf{type}$; the induction hypothesis gives formation of $S^{\prime }$, and field formation rebuilds $\{a:S^{\prime }\}$. Rules R-Mem-L and R-Mem-U apply that field-case schema to the lower and upper member bound, respectively. Rules R-And-L and R-And-R apply it to the left and right intersection component. In each instance, inversion forms the unchanged component and the induction hypothesis forms the changed component.

In R-All-Cod, inversion gives $\mathrm{\Gamma },x:S⊢U\mathsf{type}$. Apply the induction hypothesis in that extended context and rebuild the function type. In R-All-Dom, the induction hypothesis forms $S^{\prime }$ and the rule’s second premise forms $U$ under $x:S^{\prime }$; these are exactly the two premises of target function formation. In R-Rec, the displayed target-recursive-type premise is already the target formation judgment; it is necessary because changing a self type also changes the context in which its body is checked. Alpha-renaming validates the freshness premise before either binder case. These are all indexed replacement rules, so the induction is complete. ◻

Proof. Take $$\mathrm{\Gamma }=q:\mathrm{\top },p:q.\mathsf{type}\wedge \{a:\{A:\mathrm{\perp }..\mathrm{\top }\}\}.$$ Then $p.a.A$ is formed, $\mathrm{\Gamma }⊢p:q.\mathsf{type}$, and both $p$ and $q$ are paths. A root-only version of RP-Here, RP-Fld, and R-Sel would replace $p.a.A$ by $q.a.A$. But $q:\mathrm{\top }$ exposes no field $a$, so $\mathrm{\Gamma }⊬q.a\mathsf{path}$ and $q.a.A$ is not formed. The actual RP-Fld stops because its second premise is unavailable; even if that premise were bypassed, R-Sel would still require formation of the complete changed selection. Thus both checks are load bearing. ◻

Proof. Take $\mathrm{\Gamma }=p:\mathrm{\top }$ and $T=\{b:y.\mathsf{type}\}$. The record $T$ is tight: it has one field and no unequal type-member bounds. Substitution gives $T[p.a/y]=\{b:p.a.\mathsf{type}\}$. Rule P-Fld cannot derive $\mathrm{\Gamma }⊢p.a\mathsf{path}$ because $p$ has no field declaration for $a$. Therefore $p.a.\mathsf{type}$ is not formed, so no judgment $p.a;\mathrm{\Gamma }⊢d[p.a/y]:T[p.a/y]$ can be derived for any $d$. Rule Def-New rejects the instance through its body premise, without an extra explicit premise. ◻

Proof. Apply the inherited general-to-tight bridge in the inert context. Precise path typing decomposes the stored root type and follows each field selected by $p$; singleton propagation replaces aliases only after the target prefix is known to be typeable. Induct on the length of $p$ and, inside that induction, on its precise typing derivation. For a variable path $x$, environment matching gives $\gamma (x)=v$ with $\mathrm{\Gamma }⊢v:\mathrm{\Gamma }(x)$. Function canonical forms exclude an object value at the required dependent-function type, so $v=\lambda (x:S^{\prime })t$ with and $\mathrm{\Gamma },x:S⊢t:T$.

For $q.a$, invert path formation to obtain a precise field declaration for $a$ at $q$. By the outer induction hypothesis, lookup of $q$ terminates. If it terminates in an object, Lookup-Val selects the unique field body; precise object typing gives its declared type after self substitution. If it terminates in a path $r$, Lookup-Path replaces the prefix by $r$; the replacement rules preserve the selected field type, and the strict lookup chain has one fewer unresolved stored alias. Applying the inner induction to the resulting precise derivation eventually reaches a value. Function canonical forms again identify that value as a lambda and give the two stated typing comparisons. These are the variable, stored-value, and stored-path cases displayed above, so the induction is complete.

Termination is the part that DOT did not have to prove, because there lookup was a single variable dereference. Here it is recursive, and an infinite loop would be a hidden violation of progress. The decisive argument excludes a cycle in the typing context: if the direct lookup of $p$ yields another path $q$, then the context assigns $p$ the singleton type $q.\mathsf{type}$; so a cycle of paths in the execution environment would force a cycle of paths in the typing context, all of whose members carry only singleton types, and none of which can then carry a dependent-function type. The well-formedness hypothesis is what rules that out, and it is why the lemma is stated for well-formed inert contexts and not merely inert ones. ◻

Proof. We prove preservation first, strengthening it by simultaneous preservation of environment matching, context inertness, and path well-formedness. Induct on the term step. A beta root uses capture-avoiding substitution. A field root uses precise object typing to locate the unique field and substitutes the stable self path into its body. Installing a let-bound value extends $\gamma$ and $\mathrm{\Gamma }$ together; precise typing of the value makes the new entry inert, and freshness of the bound variable preserves well-formedness. A singleton replacement step applies proposition 108.4; its target-path formation premise preserves every selected type. Congruence cases use the induction hypothesis and rebuild the surrounding evaluation context. These are the beta, object, let, replacement, and congruence families of term reduction, which proves clause 3.

For progress, decompose a term under a matching inert context by its longest evaluation context. A function application whose head is a value contracts by beta. If its head is a path, lemma 108.9 either exposes a lambda through lookup or takes a strict lookup step. Object projection uses the corresponding precise object canonical form; a singleton path uses replacement only after the changed path has been formed. A let either reduces its bound expression or installs its value. Constructors are values, and no other outer term form exists. Thus a typed configuration either takes a term step or its term is a path or value.

Start with the empty execution environment and empty context; both matching and inertness hold. Iterate preservation along any finite term reduction. If term reduction is infinite, clause 1 holds by its first alternative. Otherwise progress gives a terminal path or value, and the last preservation instance supplies the inert, well-formed context asserted in clause 1.

For clause 2, extend progress by treating a terminal path as the head of lookup. A path of function type terminates by lemma 108.9; precise canonical forms give the same termination fact for object and field paths. Each lookup result is either a value or a strictly shorter unresolved alias chain. Cycles cannot have a non-singleton terminal type in a well-formed context, by the cycle argument in the preceding lemma. Hence extended reduction either continues forever or reaches a value. This proves all three clauses. ◻