ch:categories: ch:categories

Problem, invariant, and acceptance test. Build the category $\mathbf{Ctx}$ of example 141.9: contexts as objects, lists of terms as arrows, the action $e[\sigma ]$, composition $\tau \circ \sigma$, and identities. The invariant has two halves. Every arrow the program accepts as usable is well typed at its declared source and target in the sense of definition 141.1, and no action captures a free variable of the range. The acceptance test is the eleven-item list of exercise 141.23: the first composite (141.1) prints $\lambda w:\mathbf{2}.fx$; the two bracketings of exercise 141.1 print $\alpha$-equal lists; the two actions of example 141.6 agree and print an abstraction whose body is the free variable $x$; the two identity laws hold for the $\sigma$ of (141.1); the two actions of exercise 141.12 agree; the component of theorem 141.61 for $x\mathsf{tt}$ at $\mathrm{\Gamma }=f:\mathbf{2}\to \mathbf{2},x:\mathbf{2}$ applied to $f$ prints $f\mathsf{tt}$; and evaluating that family at the variable $x$ recovers $x\mathsf{tt}$; and the canonical renaming of $\mathrm{\Gamma }$ and its inverse compose to identities (proposition 141.48); substitution acts on a conditional and preserves its type; a pair of noncomposable arrows is rejected; and a seventeen-name avoid-set exercises the fresh-name boundary.

Representation. Terms are a datatype with named binders,

data Tm : Type = Var String | Lam String Ty Tm | App Tm Tm
                     | BTrue | BFalse | If Tm Tm Tm

and an arrow is a triple of its source, its target, and its components,

data Subst : Type = Subst Ctx Ctx (List Tm)

The raw constructor is private to the companion module. Its makeSubst boundary and checked composition protect uses of this representation: the constructor verifies that the two contexts have distinct declared names and that every component has its target declaration’s type; composition first validates both input arrows, verifies that the target of its first arrow is the source of its second, and returns either a checked arrow or an explicit rejection. The named corpus fixtures use the private constructor, but each is checked before it participates in a passing case. Carrying the target inside the arrow is what makes the action definable without a separate argument: the component list is zipped with the target’s variable names to form the replacement map. The alternative is de Bruijn indices, which remove renaming at binders entirely and make $\alpha$-equivalence syntactic equality. They were rejected here for one reason: the chapter’s capture instance is about renaming, and the acceptance test asks the program to show the renamed binder. A representation in which capture cannot be expressed cannot exhibit the obstruction the chapter singled out. The cost of names is the freshening function and an $\alpha$-equivalence checker; both are short.

The first version that runs. Write the type checker first, since arrows are defined by typing. It has one clause per rule of chapter 2:

typeOf : Ctx -> Tm -> Typed
let typeOf ctx term decreases structural term =
    match term
    case Var x -> lookupDecl x ctx
    case Lam x ty body ->
        match typeOf (Decl x ty :: ctx) body
        case HasType bodyTy -> HasType (TyArrow ty bodyTy)
        case Untyped why -> Untyped why
    case App f a -> ...   -- require f : dom -> cod and a : dom
    case If guard yes no ->
        ...               -- require guard : Bool and equal branch types

Then define wellTyped on an arrow by checking the two contexts and each component against the corresponding declared type of the target. makeSubst uses this predicate rather than leaving it to callers. It validates $\sigma =(fx):\mathrm{\Gamma }⟶\mathrm{\Delta }$ and rejects a list with a wrong type before returning an arrow.

The cases of the metatheory. The action is simultaneous substitution, and its cases are the cases of the proof of lemma 141.5. The variable case looks up the replacement map, leaving unbound names unchanged; application and the three subterms of a conditional distribute. The binder case is the one the printed proof singled out:

    case Lam x ty body ->
        let inner = dropBind x binds
        let avoid = union (rangeVars inner)
                          (union (domainVars inner) (freeVars body))
        let y = fresh (1 + nameCount avoid) x avoid
        if y == x then Lam x ty (act body inner)
        else Lam y ty (act body (Bind x (Var y) :: inner))

The avoid-set is finite. If it has $n$ elements, the $n+1$ distinct candidates $x,x^{\prime },\dots ,x^{(n)}$ cannot all belong to it, so 1 + nameCount avoid is both a termination measure and a sufficient search bound. The acceptance test uses the seventeen candidates that would have exhausted the former fixed bound of $16$. Three decisions are visible here and each answers to the proof. First, the bound name is removed from the map (dropBind) because the abstraction clause substitutes only for the free occurrences. Second, the avoid-set contains the free variables of the range, which is the freshness condition of convention 2.3; it also contains the domain and the body’s own free variables, so that renaming cannot create a new capture. Third, when renaming is needed, the body is substituted with $x\mapsto y$ added to the map, which renames and substitutes in one pass rather than renaming first and substituting second. After validating both input arrows and checking that the middle contexts are equal, composition acts with $\sigma$ on each component of $\tau$ and builds the result through makeSubst; a mismatch returns Noncomposable without constructing an arrow. The identity is the list of the context’s variables. The Yoneda component of a term $x:A⊢b:B$ at $\mathrm{\Gamma }$ applied to $e$ is the action of the one-element substitution $(e):\mathrm{\Gamma }⟶⟨A⟩$ on $b$, and its recovery evaluates the component at $⟨A⟩$ on the variable $x$; both are two-line definitions on top of the action. The canonical renaming of a context lists its variables as the components of a substitution into the context with the same types under the names $x_1,x_2,\dots$, and its inverse lists $x_1,x_2,\dots$ in turn; the equivalence case composes them both ways and compares with the identities. Add the $\alpha$-equivalence checker last: it walks two terms with a list of bound-name pairs, and a free variable matches only itself.

The failure the reader will hit. Delete the freshening: replace let y = fresh (1 + nameCount avoid) x avoid by let y = x. The program still typechecks, the first composite still prints $\lambda w:\mathbf{2}.fx$, and the associativity and identity cases still pass, because none of their binders collides with a range variable. Only the capture case fails, printing $\lambda x:\mathbf{2}.x$: the free $x$ of $\mathrm{\Gamma }$ has been captured and the result is a closed term, exactly the failure of example 141.6. That one case is the only evidence in the corpus that renaming is implemented at all. A second instructive mutation composes in the wrong order, acting on $\sigma$’s components with $\tau$. The checked constructor rejects the malformed result in the first composite, associativity, the right identity, the seminar composite, and one direction of the equivalence. The rejection occurs at the invariant boundary instead of allowing a malformed arrow to flow into later calculations.

Discharging the acceptance test. Run the corpus with the command recorded in appendix E. The eleven case lines, followed by the summary, are

PASS first composite: (\w:Bool. f x)
PASS associativity instance: ((\w:Bool. f x) false) both ways
PASS capture instance: \x':Bool. x keeps x free
PASS identity laws: id.sigma = sigma = sigma.id
PASS seminar binder composite: action law holds
PASS Yoneda component: f true
PASS Yoneda recovery: x true
PASS named/nameless equivalence: (f, x) inverts (x1, x2)
PASS conditional action: if true then f x else false
PASS rejected noncomposable arrows
PASS fresh-name boundary avoids 17 forbidden names
All 11 Chapter 141 corpus cases passed.

Check each against the chapter: the first composite is (141.1), with the bound name $w$ unchanged because $w$ is not free in $fx$; the associativity line is exercise 141.1; the capture line is example 141.6 with the renamed binder $x^{\prime }$ and the free body $x$; the Yoneda lines are the two directions of theorem 141.61 on $b=x\mathsf{tt}$, the component being $b[f/x]$ and the recovery being the component at $⟨\mathbf{2}\to \mathbf{2}⟩$ applied to the variable $x$; the named/nameless line is the equivalence of proposition 141.48 on one context, the two renamings being checked to compose to identities rather than merely to be well typed. The conditional line exercises the constructor omitted by the earlier subcalculus. The rejection line checks the typed boundary of composition, and the final line checks the sufficient fresh-name bound rather than one friendly capture instance.

What the program does not prove. The run shows that the substitution algebra behaves as proposition 141.7 says on the named inputs, rejects one ill-matched composition boundary, exercises every term constructor, checks one Yoneda bijection on one term, and checks that one renaming is invertible. It does not prove lemma 141.5, which quantifies over all terms and all substitutions, and it does not prove theorem 141.52; the first is proved in the chapter by induction and the second by calculation.