Chapter 107Optional

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

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

An existential package can hide a representation type, but a client cannot name that type in the result of a second method after the package has been opened and closed. A family-polymorphic object needs a persistent name. If $x$ denotes the object and $A$ denotes its abstract type member, the client needs the type $x . A$ . Bounds make that name useful: $x : {A : S . . U} ⟹ S <: x . A <: U .$ The same two inequalities also create the central obstruction. An arbitrary assumption $x : {A : ⊤ . . ⊥}$ yields $⊤ <: ⊥$ and collapses every pair of types. The soundness proof must therefore distinguish hypotheses written in a function body from hypotheses justified by values at run time.

A variable-path DOT calculus

Definition 107.1 — Syntax and the receiver binder ¶

The selected calculus is A-normal and restricts paths to variables. Its types, terms, values, and definitions are $\begin{array}{rcl} T, U & ::= & ⊤ ∣ ⊥ ∣ {a : T} ∣ {A : S . . U} \\ ∣ & T \land U ∣ \forall (x : S) U ∣ μ (x : T) ∣ x . A . \end{array}$ $\begin{array}{rcl} t, u & ::= & x ∣ λ (x : T) . t ∣ x y ∣ x . a ∣ ν (x : T) d ∣ let x = t in u, \\ v & ::= & λ (x : T) . t ∣ ν (x : T) d, \\ d & ::= & {a = t} ∣ {A = T} ∣ d \land d . \end{array}$ Labels combined by $d_{1} \land d_{2}$ are disjoint. In the recursive object type $μ (x : T)$ , $x$ binds a term receiver that may occur in $T$ . In the object value $ν (x : T) d$ , the same receiver names the object while checking $d$ . This binder is not the recursive type variable $X$ in $μ X . R (X)$ , not the OO family type Self, not a same-subject intersection binder, and not an identity path.

Referenced from 3 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

The first family object stores an abstract element type and a value of that type: $Cell = μ (c : {A : ⊥ . . ⊤} \land {v a l u e : c . A}) .$ An implementation with representation $N$ is $ν (c : {A : N . . N} \land {v a l u e : c . A}) ({A = N} \land {v a l u e = 0}) .$ After binding this value to $n$ , a client may project $n . v a l u e : n . A$ without learning that $n . A = N$ . The type member persists as the path-dependent name that the existential encoding lacked.

Definition 107.2 — Typing and subtyping delta ¶

Term typing uses the following six ordinary rules

Γ (x) = T

Γ ⊢ x : T

DOT-Var

Γ, x : T ⊢ t : U

x \notin fv (T)

Γ ⊢ λ (x : T) . t : \forall (x : T) U

DOT-All-I

Γ ⊢ x : \forall (z : S) T

Γ ⊢ y : S

Γ ⊢ x y : T [y / z]

DOT-All-E

Γ ⊢ t : T

Γ, x : T ⊢ u : U

x \notin fv (U)

Γ ⊢ let x = t in u : U

DOT-Let

Γ ⊢ x : T

Γ ⊢ x : U

Γ ⊢ x : T \land U

DOT-And-I

Γ ⊢ t : T

Γ ⊢ T <: U

Γ ⊢ t : U

DOT-Sub

and the ordinary subtyping lattice

Γ ⊢ T <: ⊤

DOT-Top

Γ ⊢ ⊥ <: T

DOT-Bot

Γ ⊢ T <: T

DOT-Refl

Γ ⊢ S <: T

Γ ⊢ T <: U

Γ ⊢ S <: U

DOT-Trans

Γ ⊢ T \land U <: T

DOT-And_1-

Γ ⊢ T \land U <: U

DOT-And_2-

Γ ⊢ S <: T

Γ ⊢ S <: U

Γ ⊢ S <: T \land U

DOT–And

Γ ⊢ T <: U

Γ ⊢ {a : T} <: {a : U}

DOT-Fld–Fld

The delta that makes the calculus dependent consists of the following rules.

Γ ⊢ x : {A : S . . U}

Γ ⊢ S <: x . A

DOT-Sel-L

Γ ⊢ x : {A : S . . U}

Γ ⊢ x . A <: U

DOT-Sel-U

Γ ⊢ S_{2} <: S_{1}

Γ ⊢ U_{1} <: U_{2}

Γ ⊢ {A : S_{1} . . U_{1}} <: {A : S_{2} . . U_{2}}

DOT-Type-Mem-Sub

Dependent-function subtyping is the displayed rule

Γ ⊢ S_{2} <: S_{1}

Γ, x : S_{2} ⊢ T_{1} <: T_{2}

Γ ⊢ \forall (x : S_{1}) T_{1} <: \forall (x : S_{2}) T_{2}

DOT-Π-Sub

Γ ⊢ x : T

Γ ⊢ x : μ (x : T)

DOT-Rec-I

Γ ⊢ x : μ (z : T)

Γ ⊢ x : T [x / z]

DOT-Rec-E

Γ, x : T ⊢ d : T

Γ ⊢ ν (x : T) d : μ (x : T)

DOT-Obj-I

Γ ⊢ x : {a : T}

Γ ⊢ x . a : T

DOT-Fld-E

Definition typing contains

Γ ⊢ {A = T} : {A : T . . T}

DOT-Def-Type

Γ ⊢ t : T

Γ ⊢ {a = t} : {a : T}

DOT-Def-Val

Γ ⊢ d_{1} : T_{1}

Γ ⊢ d_{2} : T_{2}

dom (d_{1}) \cap dom (d_{2}) = \emptyset

Γ ⊢ d_{1} \land d_{2} : T_{1} \land T_{2}

DOT-Def-And

Thus dependent-function subtyping is contravariant in the domain and compares the codomains under the smaller domain. The calculus has no subtyping rule between two recursive types. Recursion is introduced and eliminated through typing, which is one source of cycles in typing derivations.

Compare the two binders. DOT-All-I requires $x \notin fv (T)$ , because the parameter type is checked before the parameter is bound; its codomain $U$ may depend on $x$ . By contrast, DOT-Let requires $x \notin fv (U)$ , because the result type escapes the let binder. DOT-Obj-I carries neither premise, and it must not: the receiver $x$ is exactly what $T$ is allowed to mention, and $μ (x : T)$ retains the binder in the conclusion. A freshness condition on DOT-Obj-I would make every object whose member type selects its own receiver untypable.

Referenced from 8 locations

Put $d_{N} = {A = N} \land {v a l u e = 0}$ and $T = {A : N . . N} \land {v a l u e : c . A}$ . The implementation above has the two-stage derivation $\frac{\begin{matrix} Γ, c : T ⊢ {A = N} : {A : N . . N} \\ Γ, c : T ⊢ {v a l u e = 0} : {v a l u e : c . A} \end{matrix}}{Γ, c : T ⊢ d_{N} : T} DOT - Def - And .$ Consequently, $\frac{Γ, c : T ⊢ d_{N} : T}{Γ ⊢ ν (c : T) d_{N} : μ (c : T)} DOT - Obj - I .$ The field-definition premise uses DOT-Sel-L and subsumption to derive $0 : c . A$ . A neutral projection $x . a$ has no reduction until a surrounding let binds $x$ to an object value.

Exercise 107.1 ¶

★★☆ Bind the displayed cell implementation to $n$ . Derive $n . v a l u e : n . A$ and $n . A <: N$ . Then replace the declaration by ${A : ⊥ . . ⊤}$ and identify the exact derivation step that no longer gives $n . A <: N$ .

Referenced from 3 locations

Bad bounds forbid global inversion

Proposition 107.3 — Collapse under a bad bound ¶

In the context $Γ = x : {A : ⊤ . . ⊥}$ , one has $Γ ⊢ S <: U$ for every well-formed pair of types $S, U$ .

Referenced from 4 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

Proof of Proposition 107.3 — Collapse under a bad bound

Proof. The declaration $x : {A : ⊤ . . ⊥}$ makes both selection rules applicable to the same member, so DOT-Sel-L and DOT-Sel-U give $Γ ⊢ ⊤ <: x . A$ and $Γ ⊢ x . A <: ⊥$ . One use of DOT-Trans between them gives $\begin{matrix} (*) & Γ ⊢ ⊤ <: ⊥ . \end{matrix}$ The chain $\begin{aligned} S & \overset{D O T - T o p}{<:} ⊤ \overset{(*)}{<:} ⊥ \overset{D O T - B o t}{<:} U \end{aligned}$ then yields $Γ ⊢ S <: U$ by two further uses of DOT-Trans. ◻

The assumption is well formed: $⊥ <: ⊤$ . It need not be inhabited by an object value. Definition typing assigns a concrete member only the tight declaration ${A : T . . T}$ . A proof that globally inverts every well-formed context would therefore reason from assumptions that no run-time object can justify. Ordinary global narrowing and a transitivity proof based on such inversion are the wrong induction hypotheses.

Exercise 107.2 ¶

★☆☆ Delete the lower selection rule from proposition 107.3 and construct a two-element subtype lattice in which the remaining premises hold but $⊤ <: ⊥$ fails. Repeat after restoring DOT-Sel-L and deleting DOT-Sel-U.

Referenced from 3 locations

Inert contexts and tight typing

Run-time values force a syntactic repair. A function value has a dependent function type. An object value has a recursive type whose concrete type members have equal bounds.

Definition 107.4 — Inert type and inert context ¶

An inert type is either a dependent function $\forall (x : S) T$ or a recursive type $μ (x : T)$ such that $T$ is an intersection of field declarations ${a : S}$ and tight type declarations ${A : S . . S}$ with pairwise distinct type labels. A context is inert if every declaration assigns an inert type.

Referenced from 2 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

The type $μ (c : {A : N . . N} \land {v a l u e : c . A})$ is inert. The type $μ (c : {A : ⊥ . . ⊤})$ is not: its member bounds differ. Inertness does not assert inhabitation; for example, $\forall (x : ⊤) ⊥$ is inert and has no closed value in the calculus.

Definition 107.5 — Precise and tight typing ¶

A precise variable judgment $Γ ⊢_{!} x : T$ starts from $T = Γ (x)$ and eliminates outer recursive types and intersections. It never applies subsumption. The tight typing judgment $Γ ⊢_{#} t : T$ has the general DOT rules except that type selection requires an equal-bounds precise declaration:

Γ ⊢_{!} x : {A : T . . T}

Γ ⊢_{#} T <: x . A

DOT-T-Sel-L

Γ ⊢_{!} x : {A : T . . T}

Γ ⊢_{#} x . A <: T

DOT-T-Sel-U

Rules whose premises do not extend the context use tight premises. Lambda, let, and object introduction use general typing in the extended context, because their written parameter type need not be inert.

Tight typing still contains cycles, because DOT-Sub may both widen and narrow. Stratify it once more; the recipe is worth stating because it explains the variable-or-value restriction in theorem 107.9. Delete every elimination rule; specialize what remains to variables and values; and take the leaves from precise typing, which keeps only the rules that decompose $Γ (x)$ . What survives is the invertible typing judgment $Γ ⊢_{# #} t : T$ : recursion introduction, intersection introduction, DOT-Top, tight selection, and the three covariance rules for fields, type members, and dependent functions. Every one of them builds a larger type from a smaller one, and none consumes a type it has just built, so induction on $⊢_{# #}$ terminates and each derivation exposes the outer form of its subject.

Because the second step of the recipe specializes to variables and values, $⊢_{# #}$ is defined only for those. That is not a technicality to be optimized away: it is why the bridge from tight typing carries a variable-or-value hypothesis, and it is enough, because canonical forms are asked only about variables and values.

Referenced from 2 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

Tight selection cannot reproduce the bad-bounds derivation: a precise declaration ${A : T . . T}$ gives only $T <: x . A <: T$ . The restriction would be too weak for arbitrary DOT programs, but it loses no derivation in an inert context.

Lemma 107.6 — Tight-to-invertible bridge ¶

If $Γ$ is inert, $t$ is a variable or value, and $Γ ⊢_{#} t : T$ , then $Γ ⊢_{# #} t : T$ .

Referenced from 5 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

Proof of Lemma 107.6 — Tight-to-invertible bridge

Proof. Induct simultaneously on the tight typing derivation and on each tight subtyping premise used by its final rule. A precise-variable leaf is already an invertible leaf. Rules for recursion introduction, intersection introduction, top, and covariance of fields, type members, and dependent functions rebuild the corresponding invertible rule from the induction hypotheses.

Elimination rules require inversions of the induction hypothesis rather than new invertible eliminators. For recursion elimination, the induction hypothesis for the premise ends in recursion introduction, so inversion returns its body type after self substitution. For either intersection projection, the premise ends in intersection introduction, and inversion selects the requested component. A subsumption conclusion uses the typing induction hypothesis for its subject and the simultaneous subtyping induction hypothesis for the comparison. Tight selection has a precise equal-bounds premise; its two rules therefore rebuild the same selected type from that precise leaf. A lambda, let, or object-introduction derivation can contribute only when its conclusion is a value, in which case the rule’s general premise is retained exactly as required by the invertible introduction rule. Application and field elimination cannot conclude a typing judgment for a syntactic variable or value. These cases cover every tight rule family and establish both simultaneous claims. ◻

Lemma 107.7 — Selection replacement ¶

Let $Γ$ be inert. If $Γ ⊢_{#} x : {A : S . . U}$ , then there is a type $T$ such that $Γ ⊢_{!} x : {A : T . . T}, Γ ⊢_{#} S <: T, Γ ⊢_{#} T <: U .$ Consequently $Γ ⊢_{#} S <: x . A$ and $Γ ⊢_{#} x . A <: U$ .

Referenced from 4 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

Proof of Lemma 107.7 — Selection replacement

Proof. Apply lemma 107.6, then induct on the resulting invertible derivation of $Γ ⊢_{# #} x : {A : S . . U}$ . A precise-variable leaf starts from $Γ (x)$ . Since $Γ$ is inert, recursion elimination and intersection elimination reach a unique declaration ${A : T . . T}$ ; unequal bounds cannot occur in an inert recursive object type. This gives $Γ ⊢_{!} x : {A : T . . T}$ . The covariance rule for a type-member declaration changes its lower bound only by a premise $S <: T$ and its upper bound only by a premise $T <: U$ . Recursive and intersection introduction preserve those two premises. No other invertible rule concludes a type-member declaration. The induction therefore yields $S <: T$ and $T <: U$ in every case. Applying DOT-T-Sel-L and DOT-T-Sel-U yields $S <: T <: x . A and x . A <: T <: U,$ and tight transitivity gives the two conclusions. ◻

Theorem 107.8 — General typing becomes tight in an inert context ¶

If $Γ$ is inert, then $Γ ⊢ t : T ⟹ Γ ⊢_{#} t : T, Γ ⊢ S <: U ⟹ Γ ⊢_{#} S <: U .$

Referenced from 3 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

Proof of Theorem 107.8 — General typing becomes tight in an inert context

Proof. Use mutual rule induction on general typing and subtyping. The induction hypotheses state the two displayed implications for every premise whose context is still $Γ$ . Variable, application, projection, recursion, intersection, top, bottom, declaration, and subsumption cases rebuild the corresponding tight rule from those hypotheses. Dependent-function subtyping applies the induction hypothesis to the domain premise; its codomain premise extends the context, so the tight rule, like the definition, uses the general premise there. Lambda, let, and object introduction also retain their general extended-context premises. Only DOT-Sel-L and DOT-Sel-U lack tight counterparts. For those two cases, lemma 107.7 supplies the tight conclusions. This list exhausts the rule families. ◻

If inertness is deleted, the bad-bound context in proposition 107.3 derives $⊤ <: ⊥$ generally, while tight typing cannot derive it. Thus the theorem’s substantive hypothesis is not removable.

Canonical forms and the safety interface

Tight typing still contains introduction/elimination cycles. Splitting it into precise elimination followed by invertible introduction makes the outer form of a run-time value recoverable by induction.

Theorem 107.9 — Canonical forms in inert contexts ¶

Let $Γ$ be inert.

If $Γ ⊢ z : \forall (x : T) U$ , then $Γ (z) = \forall (x : T^{'}) U^{'}$ for some $T^{'}$ and $U^{'}$ with $Γ ⊢ T <: T^{'}$ and $Γ, x : T ⊢ U^{'} <: U$ .
If $Γ ⊢ v : \forall (x : T) U$ , then $v = λ (x : T^{'}) . t$ for some $T^{'}$ and $t$ with $Γ ⊢ T <: T^{'}$ and $Γ, x : T ⊢ t : U$ .
If $Γ ⊢ x : {a : T}$ , then $Γ (x) = μ (x : S)$ where $S$ is an intersection one of whose components is ${a : T^{'}}$ , and $Γ ⊢ T^{'} <: T$ .
If $Γ ⊢ v : μ (x : S)$ and $S$ is an intersection one of whose components is ${a : T}$ , then $v = ν (x : S) d$ where $d$ is an intersection one of whose components is ${a = t}$ , and $Γ ⊢ t : T$ .

Referenced from 6 locations

Proof of Theorem 107.9 — Canonical forms in inert contexts

Proof. By theorem 107.8, each premise has a tight derivation. The subject is a variable or a value, so lemma 107.6 gives an invertible derivation.

For clause 1, precise decomposition of $Γ (z)$ removes outer recursive types and intersections. Inertness leaves either a dependent-function entry or an equal-bounds recursive-object entry. Only the first can acquire the outer type $\forall (x : T) U$ in the invertible judgment. Its declaration is $\forall (x : T^{'}) U^{'}$ , and the covariance premises accumulated while rebuilding the type are $T <: T^{'}$ and, under $x : T$ , $U^{'} <: U$ .

For clause 2, induct on the invertible typing of $v$ . Recursive and intersection introductions preserve the induction hypothesis. Tight selection cannot be the base rule for a value of function type, because its precise premise is a variable judgment. Thus the base rule is DOT-All-I, which gives $v = λ (x : T^{'}) . t$ , $T <: T^{'}$ , and $Γ, x : T^{'} ⊢ t : U^{'}$ . Narrowing along $T <: T^{'}$ gives $Γ, x : T ⊢ t : U^{'}$ , and DOT-Sub along $U^{'} <: U$ gives the stated body judgment.

Clause 3 uses the first phase of clause 1. Precise decomposition of $Γ (x)$ reaches the unique field declaration ${a : T^{'}}$ in its inert recursive intersection, and the field covariance premises compose to $T^{'} <: T$ . For clause 4, the invertible derivation cannot end at a function introduction. Its base is DOT-Obj-I, so $v = ν (x : S) d$ ; intersection decomposition locates the unique definition ${a = t}$ , and inversion of DOT-Def-And and DOT-Def-Val gives $Γ ⊢ t : T$ . These are all invertible base rules, proving the four clauses. ◻

The runtime is A-normal. Evaluation contexts contain let bindings of values. The critical roots are $\begin{aligned} E [x y] & ⟶ E [t [y / z]] & if E binds x = λ (z : S) t, \\ E [x . a] & ⟶ E [t] & if E binds x = ν (z : T) d \\ and d contains {a = t}, \\ E [let x = y in t] & ⟶ E [t [y / x]] . \end{aligned}$

Theorem 107.10 — Structural and safety theorem for simple DOT ¶

For the exact syntax and reduction of definition 107.1, definition 107.2:

if $Γ (x) = T$ and $Γ [x : T^{'}] ⊢ T^{'} <: T$ , then $Γ ⊢ t : U$ implies $Γ [x : T^{'}] ⊢ t : U$ , and $Γ ⊢ S <: U$ implies $Γ [x : T^{'}] ⊢ S <: U$ ;
if $Γ, x : S ⊢ t : T$ and $Γ ⊢ y : S [y / x]$ , then $Γ ⊢ t [y / x] : T [y / x]$ ;
if $Γ$ is inert, $t$ is a variable or a value, and $Γ ⊢_{#} t : T$ , then $Γ ⊢_{# #} t : T$ ;
if $\cdot ⊢ t : T$ , then $t$ is a normal form or takes a step;
if $\cdot ⊢ t : T$ and $t ⟶ t^{'}$ , then $\cdot ⊢ t^{'} : T$ .

Referenced from 2 locations

Dependent Object Types: Type Members, Bad Bounds, and Recursive Self

Proof of Theorem 107.10 — Structural and safety theorem for simple DOT

Proof. For clause 1, use mutual induction on typing and subtyping. A variable case uses the narrowed declaration $T^{'}$ and subsumption along $T^{'} <: T$ . Dependent-function subtyping applies the induction hypothesis to its domain and codomain premises; alpha-rename its binder away from $x$ first. Recursive types and intersections apply the induction hypotheses componentwise. Selection uses lemma 107.7; all remaining rules rebuild directly. These are the binder, selection, conversion, and structural rule families, so the mutual induction is complete.

For clause 2, use mutual induction on the derivations of typing, subtyping, and precise typing. The variable equal to $x$ uses the supplied judgment for $y$ ; every other variable is unchanged. Under a lambda, let, recursive type, or object self binder, choose the binder outside $FV (y) \cup FV (T) \cup dom (Γ)$ and apply the induction hypothesis to the renamed body. Application and field selection use the induction hypotheses on their subjects. Type selection commutes with substitution because paths are variables in this calculus. Intersection, recursion, and subsumption rebuild their rules. Thus every syntax and rule family is covered.

Clause 3 is lemma 107.6.

For progress, decompose a closed term as its longest evaluation context $E [r]$ . The values bound by $E$ determine a runtime context $Γ_{E}$ . Each value has a precise inert type, so $Γ_{E}$ is inert. If $r = x y$ , clauses 1–2 of theorem 107.9 show that $x$ is bound by $E$ to a lambda, and the application root applies. If $r = x . a$ , clauses 3–4 show that $x$ is bound to an object with a unique $a$ definition, and the projection root applies. A let with a value applies its let root. If no such redex exists, the term is a normal form. These cases exhaust the A-normal runtime.

For preservation, use the same decomposition. In the application case, canonical forms give a lambda $λ (z : S) t$ and the codomain comparison; clause 2 types $t [y / z]$ , and subsumption gives the redex’s result type. In the projection case, precise object typing and disjoint labels give the unique definition ${a = t}$ with the required field type. In the let case, clause 1 narrows the written binder type to the precise inert type of the installed value, after which clause 2 performs substitution. Rebuilding the typing derivation of $E [-]$ preserves the outer result type. This proves clauses 4–5 and completes the theorem. ◻

Exercise 107.3 ¶

★★★ Consider the application root $E [x y] ⟶ E [t [y / z]]$ . Starting from an inert context extracted for $E$ , use clauses 1 and 2 of theorem 107.9 to recover the lambda bound to $x$ . State the exact variable-substitution judgment needed to type $t [y / z]$ , including the codomain substitution. Explain where the proof would stop if the extracted context were not inert.

Referenced from 3 locations

What has and has not been decided

The declarative rules contain transitivity, recursive typing cycles, and path-dependent selection. Soundness does not make them an algorithm. In particular, full D-subtyping with lower and upper bounds is undecidable. Kernel D-subtyping is decidable by the Step algorithm, strong-kernel D-subtyping is decidable by Stare-at, and full D-subtyping and full term typing are undecidable. The variants that retain subtyping reflection while restricting dependent-function subtyping remain open. The earlier one-direction reduction from System F with bounded quantification does not establish the undecidability result.

No theorem in this chapter states decidability of full DOT typing, subtyping, or inference. A checker for an annotated fragment would require a separate syntax-directed relation, a termination measure, and soundness and completeness proofs. The finite decision problem in the seminar checks only the inertness precondition and selection chains.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 107.4, then complete exercise 107.8.

Exercise 107.4 ¶

★☆☆ Compute whether each type is inert: $\forall (x : S) T$ , $μ (x : {A : S . . S} \land {a : x . A})$ , and $μ (x : {A : S . . U})$ with $S \neq U$ . State the clause used in each decision.

Referenced from 4 locations

Exercise 107.5 ¶

★★☆ Starting from $x : μ (z : {A : T . . T} \land {a : z . A})$ , derive $x . a : x . A$ . Display DOT-Rec-E, intersection elimination, DOT-Fld-E, and the two tight selection bounds.

Referenced from 3 locations

Exercise 107.6 ¶

★★☆ Construct the bad-bounds collapse for two distinct closed record types $S$ and $U$ . Then prove that no object definition typed by DOT-Def-Type contributes the unequal declaration ${A : ⊤ . . ⊥}$ to an inert runtime context.

Referenced from 3 locations

Exercise 107.7 ¶

★★★ Reconstruct the object-projection case of preservation. Name the precise recursive type of the object value, locate its unique field label using disjointness, and rebuild the surrounding let context.

Referenced from 3 locations

Exercise 107.8 ¶

★★★ Practical project.dot-inert-selection-checker

Implement in Kappa a finite representation of dependent-function and recursive-object context entries. Check that recursive entries contain pairwise distinct field labels and only equal-bounds type members. For an accepted entry, calculate the tight selection chain $T <: x . A <: T$ . The invariant is that no unequal-bounds member reaches the selection calculator. The acceptance test must accept the cell context, reject ${A : ⊤ . . ⊥}$ , reject a duplicate label, print the two equal-bound selection steps, reject lookup of a missing member, and report that a dependent-function entry has no type-member selection. The named outcomes are cell context accepted, bad bounds rejected, lower tight selection printed, upper tight selection printed, missing member lookup rejected, and function entry has no member selection. A mutation that ignores the upper-bound equality must leave the Kappa source well typed but fail both the bad-bounds and unequal-bound oracles. Identify the exact DOT-T-Sel-U premise lost by that mutation.

Referenced from 5 locations

Sources. Rapoport, Kabir, He, and Lhoták give the calculus, its Figure 2 rules, and the inert-context safety package in Lemmas 3.7–3.11 and 3.19 and Theorems 3.6 and 3.17–3.18 [RKHL17]. Rompf and Amin give the earlier rich-DOT proof [RA16]; Hu and Lhoták give the corrected D-subtyping decision boundary [HL20]. Each source proof package is shorter than ten pages and is proved locally.