appendix sectiontutorials

ch:system-f: ch:system-f

Problem and result. Implement exactly the five System F term constructors, return replayable typing evidence, and enumerate every compatible one-step beta reduct. The finished checker first checks that every type in its term context is formed at the supplied type depth. It then validates the term and type substitutions, the polymorphic identity, the expanded Church-product eta boundary, and preservation on a finite reduction suite.

Representation. Use separate de Bruijn indices for the two namespaces:

data Ty : Type =
    TyVar Nat | Arrow Ty Ty | Forall Ty
data Term : Type =
    Var Nat | Lam Ty Term | App Term Term
    | TLam Term | TApp Term Ty
data Derivation : Type =
    DVar Nat Ty | DLam Ty Ty Derivation
    | DApp Ty Ty Derivation Derivation
    | DTLam Ty Derivation | DTApp Ty Ty Derivation
data Checked : Type = Checked Ty Derivation

There are no binder names to compare or duplicate. Alpha-equivalent named inputs elaborate to identical trees. A type index below the cutoff is bound; an index at or above it is free relative to that cutoff. Thus entering Forall raises the type cutoff, entering Lam raises the term cutoff, and entering TLam weakens every type in the term context. The external constructor UnannotatedSelf belongs to a separate Surface datatype, so rejection cannot accidentally extend the object language.

First complete checker. Implement wellTy, and let wellContext d Gamma check every type in Gamma at depth d. Both infer and valid Derivation reject before inspecting a term when this test fails; replay also rejects an ill-formed expected type. Then implement de Bruijn context lookup and the five clauses of infer. The TLam clause checks its body at type depth $d + 1$ under the weakened term context and returns

Checked (Forall bodyTy)
        (DTLam bodyTy evidence)

The TApp clause first forms its argument, requires a Forall bodyTy operator, and returns

Checked (substTyAt 0 argument bodyTy)
        (DTApp bodyTy argument evidence)

Put $\begin{aligned} p & : = TLam (Lam (TyVar 0) (Var 0)), \\ I & : = \forall X . X \to X . \end{aligned}$ Now check $TApp p I$ . The result is $I \to I$ , and its type-beta reduct is $Lam I (Var 0)$ .

Implement validDerivation as a separate recursion on the evidence tree. It pattern-matches the supplied term and expected type and rechecks the premises of the recorded rule; it never calls infer. A DVar falsely offered for the polymorphic identity must be rejected. This makes the invariant executable: every accepted term context and returned type are formed at the supplied type depth, and every accepted term carries a derivation that replays independently. In particular, infer 0 [TyVar 0] (Var 0) and a matching forged replay both fail.

Capture-avoiding substitutions. For type substitution at depth $d$ , replace index $d$ by the replacement shifted through $d$ binders, decrement indices above $d$ , and leave lower indices fixed. Recurse below Forall at $d + 1$ . Apply the same operation to every annotation and type argument in a term, raising $d$ below TLam. Term substitution uses the identical three-way index test, raises its depth below Lam, and leaves the depth unchanged below TLam. Require the two capture probes $\begin{aligned} [0 \mapsto Var 0] (Lam I (Var 1)) & = Lam I (Var 1), \\ [0 \mapsto TyVar 0] (Forall (TyVar 1)) & = Forall (TyVar 1) . \end{aligned}$ In each result, index $1$ denotes the replacement that remains free beyond the newly crossed binder; index $0$ would exhibit capture.

Compatible reduction and the eta boundary. Return a list rather than one evaluator successor. A variable returns the empty list. A lambda maps Lam domain over all body reducts. Application concatenates reducts from its operator and argument and prepends the root term-beta reduct when its operator is a lambda. Type abstraction maps TLam over body reducts. Type application maps TApp argument over operator reducts and prepends the root type-beta reduct when its operator is a type abstraction. No value restriction is present. Re-infer every member of every returned list and replay its evidence against the source type.

Do not add primitive products. With $P = \forall X . (I \to I \to X) \to X$ and $p : P$ , construct the long eta candidate as the exact de Bruijn encoding of $Λ X . λ k : I \to I \to X . k (p [I] (λ a : I . λ b : I . a)) (p [I] (λ a : I . λ b : I . b)) .$ Check it and the short candidate $p$ under the same context. Both reduct lists must be empty and their structural trees must differ.

A failing version. Apply mutant-no-lambda-descent.patch to a disposable copy. It changes the lambda clause of immediateReducts to the empty list. The program still passes kappa check. The input $λ x : I . (λ y : I . y) (Λ X . λ z : X . z)$ then loses its body reduct, so the compatible-constructor oracle prints FAIL and the aggregate changes to Chapter 9 corpus failed.

Acceptance test and mathematical boundary. From artifacts/ch9-system-f-checker/, run

../../.local-tools/kappa/bin/kappa check corpus.kp
../../.local-tools/kappa/bin/kappa test  corpus.kp
../../.local-tools/kappa/bin/kappa run   corpus.kp
../../.local-tools/kappa/bin/kappa audit corpus.kp

The run must report the eleven named lines recorded in appendix E and end All 11 Chapter 9 corpus cases passed.; audit must be []. Apply the preserved mutation with

patch -p1 < mutant-no-lambda-descent.patch

Its check must succeed, and its test must print

FAIL compatible constructor descent
Chapter 9 corpus failed.

The source executes finite typing and reduction witnesses. It proves neither general preservation nor normalization, does not establish confluence or eta, and says nothing semantic about Reynolds’s obstruction.