appendix sectiontutorials

ch:dependent-object-types: inert selection

Problem and result. Reject every recursive context entry that could contribute bad type-member bounds, and expose tight selection only after that rejection. Acceptance requires the concrete cell context, rejection of unequal bounds and duplicate labels, and the printed equal-bound chain $T <: x . A <: T$ .

Representation. Use a sum with function entries and recursive-record entries. A recursive entry carries separate lists of field labels and member bounds. The checker computes label uniqueness and bound equality before constructing a selection result. An intrinsic inert-entry datatype could store only certificates, but the extrinsic records admit the malformed inputs needed to test the gate.

First complete version. Implement structural equality for the finite bound language and a recursive duplicate-label test. Define inert: function entries are accepted; recursive entries require both distinctLabels and equalBounds. At this stage the cell, bad-bound, and duplicate-label fixtures distinguish all three branches.

Remaining cases. Define the tight-selection calculator to accept only an entry already classified as inert. Locate the requested member and print its common bound once as the lower step and once as the upper step. Add an explicitly unequal member as a final oracle so that the calculator cannot silently bypass the inertness result.

Observable result. The run prints the eight lines in subappendix E.10 and ends All 8 Chapter 107 corpus cases passed. Both selection lines are required: printing only one bound does not witness the tight chain. The missing-member and function-entry lines ensure that selection is neither fabricated nor applied to the wrong entry form.

A failing version. Modify the recursive-entry branch so that it returns only distinctLabels and ignores equalBounds. The program still checks, but the bad-bound and unequal-bound oracles print FAIL. This mutation isolates the hypothesis used by tight selection without altering label processing.

Acceptance test. Require the exact stdout recorded in subappendix E.10 and the audit result []. The named mutation must make its test fail; restoring the equal-bounds conjunction must restore every accepted outcome. The executable record in subappendix E.10 alone stores commands, source identities, and the mutation transcript.

Mathematical boundary. The checker decides a finite syntactic precondition. It does not implement DOT typing or subtyping, and it proves none of selection replacement, general-to-tight conversion, canonical forms, progress, or preservation.