Chapter 95Optional

Very Dependent Functions

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Encode a record as a function on labels. In the record ${T : U_{0}, get : T \to Z, set : T \to Z \to T},$ the range at label $get$ mentions the value returned at the earlier label $T$ . An ordinary dependent function may let its codomain depend on the label, but not on values returned by the function at other labels. A function type for this record must therefore let its range inspect a restricted part of the function being classified.

The cycle that must be excluded

The notation ${f ∣ x : A \to B [f, x]}$ suggests that the range may inspect $f$ . Unrestricted use is circular. In ${f ∣ n : N \to (f (n) \to f (n))},$ the type of $f (n)$ depends on $f (n)$ itself. No smaller semantic object is available from which to decide the range PER.

By contrast, a finite record has an order on labels: the type field precedes the methods that mention it. At a label $a$ , the range may inspect only $f ↾ A_{< a}$ , where $A_{< a} : = {z : A ∣ z < a} .$ Well-founded induction on $<$ then constructs the range PERs.

Convention 95.1 — Hickey's frozen meaning explanation ¶

The chapter’s very-dependent function is Hickey’s extensional Nuprl/MetaPRL type ${f ∣ x : A \to B [f, x]}$ with a membership witness consisting of a strict well-founded relation $<$ on $A$ . The relation is not printed inside the type expression, but every formation and membership derivation records it. Types are interpreted by PERs on untyped programs. Type inference is undecidable; the source does not supply a general algorithm for choosing $<$ and does not derive the desired binary-method rule.

Referenced from 3 locations

Very Dependent Functions

A well-founded family of PERs

Let $R_{A}$ be the PER interpreting $A$ , and assume $<$ respects its equivalence classes. For $a \in dom (R_{A})$ , write $P_{a}$ for the PER assigned to the predecessor-function type ${g ∣ z : A_{< a} \to B [g, z]} .$ The definition of $P_{a}$ uses only $P_{z}$ with $z < a$ . Once $P_{a}$ is fixed, each $g \in dom (P_{a})$ determines a range PER $R_{B}^{g, a}$ interpreting $B [g, a / f, x]$ .

Definition 95.2 — Very-dependent function PER ¶

For a well-founded witness $(A, <)$ , define $R_{vdf} (f, f^{'}) ⟺ \forall a, a^{'} . R_{A} (a, a^{'}) \Rightarrow R_{B}^{f ↾ A_{< a}, a} (f (a), f^{'} (a^{'})) .$ The family $R_{B}$ is functional in related choices of $a, a^{'}$ and predecessor functions. Membership is $R_{vdf} (f, f)$ together with the displayed well-founded witness.

Referenced from 2 locations

Very Dependent Functions

At a minimal element $a_{0}$ , the predecessor domain is empty. A range expression may not evaluate $g (z)$ because no $z : A_{< a_{0}}$ exists. Thus the first PER is determined without recursion. If PERs have been constructed for all $z < a$ , the predecessor-function PER $P_{a}$ and then $R_{B}^{g, a}$ are determined. This is well-founded recursion on $a$ .

If the cycle above were admitted, the construction at $n$ would ask for the PER of $f (n)$ while defining that very PER. The predecessor restriction does not contain $n$ , so the expression $f (n)$ is out of scope and the range fails formation before any fixed point is attempted.

Exercise 95.1 ¶

★★☆ Let $A = {0, 1, 2}$ with the usual strict order. Suppose $B [f, 0] = N$ , $B [f, 1] = Fin (f (0) + 1)$ , and $B [f, 2] = Fin (f (0) + f (1) + 1)$ . Construct the three range PERs in order. State the predecessor restriction available at each stage and explain why the definition is well founded.

Referenced from 3 locations

Rules extracted from the semantics

The rule premises below keep the well-founded witness visible. Write $g : Pred (y)$ for $g : {g ∣ z : A_{< y} \to B [g, z]}$ .

Definition 95.3 — Very-dependent function rules ¶

The formation, introduction, elimination, computation, and extensional uniqueness rules are

Γ ⊢ A type

Γ ⊢<: A \to A \to U_{i}

{WellFounded}_{i} (A, <)

Γ, y : A, g : Pred (y) ⊢ B [g, y / f, x] type

Γ ⊢ {f ∣ x : A \to B [f, x]} type

VDF-F

{WellFounded}_{i} (A, <)

Γ, x : A, g : Pred (x) ⊢ b : B [g, x / f, x]

{Ext}_{A, B} (b)

Γ ⊢ λ x . b : {f ∣ x : A \to B [f, x]}

VDF-I

Γ ⊢ f : {f ∣ x : A \to B [f, x]}

Γ ⊢ a : A

{WellFounded}_{i} (A, <)

Γ ⊢ f (a) : B [f, a / f, x]

VDF-E

Γ ⊢ a : A

(λ x . b) (a) \equiv b [a / x] [(λ x . b) ↾ A_{< a} / g]

VDF-β

Γ ⊢ f_{1} : {f ∣ x : A \to B [f, x]}

Γ ⊢ f_{2} : {f ∣ x : A \to B [f, x]}

\forall a : A . Γ ⊢ f_{1} (a) \equiv f_{2} (a) : B [f_{1}, a / f, x]

Γ ⊢ f_{1} \equiv f_{2} : {f ∣ x : A \to B [f, x]}

VDF-Ext

The predicate ${Ext}_{A, B} (b)$ requires equal arguments and equal predecessor functions to produce equal results in the corresponding equal range PER. It is the annotation-level form of the source’s lambda equality premise.

Referenced from 3 locations

Very Dependent Functions

The constructor derivation begins at minimal inputs. Let $A = {0, 1}$ and take $0 < 1$ . Define $\begin{aligned} f (0) & = 3, & f (1) & = true, \\ B [f, 0] & = N, & B [f, 1] & = if f (0) > 0 then Bool else 0 . \end{aligned}$ At $0$ , the predecessor function has empty domain and $3 : N$ . At $1$ , the restriction contains $f (0) = 3$ , so the range computes to $Bool$ and $true$ inhabits it. Rule VDF-I therefore classifies $f$ . Application at $1$ gives $f (1) : B [f, 1] \overset{d e f i n i t i o n}{\equiv} Bool .$ Application to a neutral $a : A$ remains stuck: the range $B [f, a]$ is known to be a type, but neither the branch nor the value $f (a)$ computes.

Exercise 95.2 ¶

★★☆ Reverse the order on ${0, 1}$ in the preceding example. Show that the range at $1$ is then ill formed because it reads $f (0)$ at a nonpredecessor. Give a different range family whose dependency is accepted by the reversed order.

Referenced from 3 locations

Substitution and semantic soundness

The well-founded witness is proof data, although it is absent from the printed type. Substitution must therefore transform the witness and every predecessor restriction.

Lemma 95.4 — Restriction commutes with substitution ¶

Let $θ : Δ \to Γ$ be a context substitution. If $<$ is a strict well-founded relation on $A$ in $Γ$ , then $< [θ]$ is a strict well-founded relation on $A [θ]$ , and $(f ↾ A_{< a}) [θ] = f [θ] ↾ A [θ]_{< [θ] a [θ]} .$

Referenced from 3 locations

Very Dependent Functions

Proof of Lemma 95.4 — Restriction commutes with substitution

Proof. The substituted relation has the same relation tree with every label and term acted on by $θ$ . An infinite descending chain after substitution would map to a descending chain in the original derivation, contradicting its well-foundedness witness. Both restrictions have domain predicate $z : A [θ]$ with $z < [θ] a [θ]$ , and both apply $f [θ]$ to that $z$ , so function extensionality in the PER model gives the equation. ◻

Theorem 95.5 — Substitution for very-dependent functions ¶

Every derivable formation, membership, or equality judgment remains derivable after a well-formed context substitution.

Referenced from 2 locations

Very Dependent Functions

Proof of Theorem 95.5 — Substitution for very-dependent functions

Proof. Induct on the derivation. In VDF-F, substitute into $A$ , $<$ , and $B$ . Lemma 95.4 supplies the predecessor type used by the fourth premise, and the induction hypothesis gives formation of the substituted range. In VDF-I, the same lemma transports the body typing and ${Ext}_{A, B}$ pointwise. In VDF-E, substitute into the membership witness and argument; the result type is $B [θ] [f [θ], a [θ] / f, x]$ by capture avoidance. The extensional case applies the equality induction hypothesis at each substituted argument. ◻

Theorem 95.6 — Soundness of the extracted rules ¶

Assume the predicative PER hierarchy used by convention 95.1. The rules in definition 95.3 preserve typehood and PER membership. The semantic construction is well founded at exactly the displayed witness $(A, <)$ .

Referenced from 2 locations

Very Dependent Functions

Proof of Theorem 95.6 — Soundness of the extracted rules

Proof. Use well-founded induction on $a : A$ . The induction hypothesis supplies the PERs for every strict predecessor, hence the PER $P_{a}$ of predecessor functions. The fourth premise of VDF-F then supplies a functional range PER $R_{B}^{g, a}$ . Equation (95.1) is symmetric because the domain, predecessor-function, and range PERs are symmetric. For transitivity, use functionality to replace the middle predecessor representative before applying transitivity of the range PER. The premise of VDF-I places each result in its range PER. Rule VDF-E selects that membership fact. The beta equation is ordinary function computation with the predecessor restriction substituted for $g$ , and VDF-Ext is the definition of $R_{vdf}$ . ◻

Removing well-foundedness leaves the rule statement syntactically meaningful but invalidates the induction that constructs $P_{a}$ . Removing functionality of $R_{B}$ makes transitivity depend on the chosen representative. These are the two substantive hypotheses of the theorem.

Dependent records as ordered functions

Fix a finite list of labels $l_{0} < \dots < l_{n}$ . A dependent record type ${l_{0} : M_{0}; l_{1} : M_{1} (l_{0}); \dots; l_{n} : M_{n} (l_{0}, \dots, l_{n - 1})}$ is translated to ${f | l : Label \to case l of l_{i} \Rightarrow M_{i} (f (l_{0}), \dots, f (l_{i - 1})) ∣_\Rightarrow ⊤} .$ The label order is well founded, and the $i$ th range reads only strict predecessors. Record selection is function application.

For a point object, take $\begin{aligned} PointMethods (R) : = { & get : R \to Z; \\ set : R \to Z \to R; \\ law : \forall r : R . \forall i : Z . get (set (r, i)) = i} . \end{aligned}$ The range for $law$ may read the earlier values at $get$ and $set$ . It may not read the value at $law$ itself. With representation $R = Z$ , define $get (r) = r$ and $set (r, i) = i$ ; reflexivity proves the law.

The corresponding abstract object type is $Object (M) : = \sum_{R : U_{i}} \sum_{s : R} M (R) .$ An object implementation chooses $R$ , a state, and a dependent method record. Conversely, opening this Sigma supplies exactly those three pieces. This gives the source’s ADT/object correspondence: implementations of a signature are proofs of the existential specification, while method wrappers hide $R$ again.

Proposition 95.7 — Width subtyping ¶

Let $R^{'}$ extend the ordered record $R$ by labels placed after every label of $R$ , and suppose the shared range types agree extensionally. Then every member of $R^{'}$ is a member of $R$ by restriction to the labels of $R$ .

Referenced from 4 locations

Proof of Proposition 95.7 — Width subtyping

Proof. Let $f : R^{'}$ . For each label $l$ of $R$ , the predecessor restriction required by $R$ is the restriction of the one already validated for $R^{'}$ . The shared range type is equal by hypothesis, so VDF-E gives $f (l) : B_{R} [f, l]$ . Equation (95.1) then proves membership of the restricted function in $R$ . No premise mentions a new label, so deleting all new branches preserves every old range judgment. ◻

Insertion of a field before an old label requires a new proof: an old range may inspect all predecessors and may therefore change. Updating one field can likewise invalidate later fields. The Point law, for example, is not preserved by changing $set$ without changing its proof field.

What the constructor does not provide

An ordinary $Π$ -type permits $B (x)$ but not $B (f, x)$ . Dependent intersection adds a view of one existing subject but performs no recursion over a domain. System S substitutes a term into its own assigned type but does not define a function range by predecessor recursion. Very-dependent formation uses the fourth premise of VDF-F; none of the other formers has that premise.

The source leaves general type checking undecidable: the well-founded relation may be implicit and type equality is extensional. It also withholds the desired binary-method rule. A method whose argument has the hidden representation type of a different object cannot be typed merely from the receiver’s existential package. Well-founded label dependency does not reveal that other representation.

Exercise 95.3 ¶

★★☆ Give a binary method type $R \to R \to Bool$ inside $Object (M)$ . Open two independently packed objects and show that their representation types are $R_{1}$ and $R_{2}$ . Identify the ill-typed application that would require $R_{1} \equiv R_{2}$ .

Referenced from 3 locations

Suggested first pass.

Begin with exercise 95.4, then complete exercise 95.6.

Exercise 95.4 ¶

★★☆ Translate the Point record into a VDF type. List the predecessor labels used by each range. Then swap the order of $set$ and $law$ and locate the failed range formation judgment.

Referenced from 4 locations

Exercise 95.5 ¶

★★★ Extend Point with a color field and color-changing method. Prove width subtyping by proposition 95.7, and calculate a wrapper that updates the position while preserving the color fields. Give a counterexample to the same calculation when a new field is inserted before an old dependent law.

Referenced from 3 locations

Exercise 95.6 ¶

★★★ Practical project.very-dependent-order-checker Implement in Kappa a checker for finite VDF record declarations. Represent each field by its label and the list of fields read by its range. Maintain the invariant that every dependency is a strict predecessor in the numeric order. The checker must accept the Point declaration and the three-stage numeric example, reject a self-dependent field, reject a two-field cycle, and check the predecessor set visible at a named field. Changing the strict comparison to a non-strict one must make the test fail.

Referenced from 5 locations

Sources. Hickey introduces the record obstruction on page 4 and the exact very-dependent meaning explanation on pages 5–6 of the FOOL paper. The record translation and Point object occupy pages 7–9; the binary-method boundary is stated on page 10. The 2001 thesis’s dedicated development gives the longer MetaPRL development. The public 2026 MetaPRL checkout preserves a later itt_dfun theory, not the exact 1996 proof state. The Kappa artifact therefore checks finite dependency orders; it neither decides extensional Nuprl typehood nor proves the PER theorem [Hic96].