Universes of Datatype Descriptions and Generic Programs

Natural numbers, lists, trees, and vectors have different constructors, yet their maps and folds repeat the same recursion: preserve constant data, recurse at recursive positions, and follow sums and products. Writing that recursion once requires data that describes a datatype without being the datatype.

A regular description sublanguage

We begin with a finite-branching regular normal form. It is the fragment on which the first map, fold, traversal, and fusion calculations are carried out; the exact indexed Morris–Altenkirch–Ghani universe is added only after those programs are in hand. Fix a small sort type $I:{\mathcal{U}}_i$. The direct attempt is to call every operator $$\mathrm{\Phi }:(I\to {\mathcal{U}}_i)\to (I\to {\mathcal{U}}_i)$$ a datatype description. A generic map would then have to turn each family $h:(j:I)\to X(j)\to Y(j)$ into a map $\mathrm{\Phi }(X)(j)\to \mathrm{\Phi }(Y)(j)$, but an arbitrary $\mathrm{\Phi }$ need not provide such an action. More seriously, $\mathrm{\Phi }(X)(j):=X(j)\to A$ places the recursive family to the left of an arrow. Its fixed point would evade the strict-positivity condition of remark 28.36.

The repair records only the operations through which a recursive position may be reached. An empty constructor needs a unit code, stored data needs a constant code, and a recursive field needs a named index. Alternative constructors force sums; several fields force products. A tag whose value determines the remaining fields forces a dependent sum.

This is a book-normalized, finite-branching sublanguage, not yet the full Morris–Altenkirch–Ghani indexed universe. Sums, products, and constants are convenient derived regular codes; $\mathsf{sigma}$ stores a finite tag whose branch is selected before recursion. The principal indexed syntax and its equality-supporting subfragment impose additional constraints on these regular codes.

The recursive family occurs only as the argument of $\mathsf{X}(j)$ and then covariantly through sums, products, and Sigma types. A code such as $\mathsf{X}(j)\to A$ cannot be formed: the grammar has no constructor that places $\mathsf{X}(j)$ to the left of a function arrow. This syntactic absence is the strict-positivity check.

The chapter extends $T_0$ by one instance of the indexed-family schema from chapter 31. No equality, universe, or context rule is replaced.

The rule names Mu-form and Mu-intro are local to description fixed points. They are not the iso-recursive-type rules with similarly named mnemonics in appendix A; their indexed code-family premises distinguish the two signatures.

The regular case takes $I:=\mathbf{1}$. Suppressing its unique index, define Under $\mathsf{roll}$, the left and right summands give the familiar constructors. For example, $$\mathsf{nil}:=\mathsf{roll}(\mathsf{inl}(\star )),\mathsf{cons}(a,xs):=\mathsf{roll}(\mathsf{inr}((a,xs))).$$ For trees, put $$\mathsf{leaf}(a):=\mathsf{roll}(\mathsf{inl}(a)),\mathsf{fork}(l,r):=\mathsf{roll}(\mathsf{inr}((l,r))).$$ The ladder has so far used unit, constants, recursive positions, alternatives, and products. To force the remaining code, let a Boolean tag choose the arity: $$D_{\mathsf{Tagged}}:=\mathsf{sigma}(\mathbf{2},b.\mathsf{case}(b;\mathsf{false}.\mathsf{one};\mathsf{true}.\mathsf{X}(\star )\times \mathsf{X}(\star ))).$$ Its two layers are $(\mathsf{false},\star )$ and $(\mathsf{true},(l,r))$. The tag is retained in the layer, and its value determines whether zero or two recursive children must be supplied.

For $l,r:\mathsf{Mu}(D_{\mathsf{Tree}(A)})$, product introduction gives $(l,r):[[\mathsf{X}(\star )\times \mathsf{X}(\star )]](\mathsf{Mu}(D_{\mathsf{Tree}(A)}))$. Sum introduction and Mu-intro therefore derive $$\mathsf{fork}(l,r):\mathsf{Mu}(D_{\mathsf{Tree}(A)}).$$ At this constructor, (80.1) replaces the two $\mathsf{All}$ components by the two recursive calls. If instead $x:\mathsf{Mu}(D)(j)$ is a variable, neither ${\mathsf{out}}_j(x)$ nor ${\mathsf{ind}}_D(P,s;j,x)$ has a root computation rule; both are neutral.

Generic action, folds, and traversals

The interpretation is functorial in its recursive family. For a family of maps $h_j:X(j)\to Y(j)$, define $$u:[[D]](X)⊢{\mathsf{map}}_D(h,u):[[D]](Y).$$ by recursion on $D$. It is the identity on $\mathsf{one}$ and constants, applies $h_j$ at $\mathsf{X}(j)$, preserves the chosen summand, maps both product components, and preserves the Sigma tag while mapping its remainder.

Proof of Lemma 80.5 — Interpretation functor laws

Proof. Induct on $D$. The unit, constant, and recursive-position cases reduce to reflexivity or beta computation at $f_j,g_j$; the laws assume no equations about those maps. A sum retains its injection and uses the induction hypothesis on its payload. A product uses the two induction hypotheses and function congruence for pairing. For $\mathsf{sigma}(A,F)$, fix $a:A$; the induction hypothesis for $F(a)$ proves the second component while the first component remains $a$. These cases exhaust the code grammar. ◻

Proof of Lemma 80.6 — Congruence of description action

Proof. Induct on $D$. The recursive-position case is $p_{j,u}$. Unit and constant codes give reflexivity. A sum follows its injection, a product applies the two induction hypotheses under pairing, and a Sigma code fixes its tag $a:A$ and applies the induction hypothesis for the branch $F(a)$. ◻

Proof of Lemma 80.7 — Layer-local congruence

Proof. Induct on $D$. At $\mathsf{X}(j)$ use the supplied path. Unit and constants give reflexivity. Sums follow their injection, products use both components of the $\mathsf{All}$ witness, and Sigma codes retain their tag and use the branch induction hypothesis. ◻

Proof of Lemma 80.9 — Fold calculation

Proof. Equation (80.1) reduces the left side to ${\alpha }_j({\mathsf{refill}}_{D(j)}(u,q))$, where $q$ contains the recursive fold results. Induction on $D(j)$ proves $${\mathsf{refill}}_{D(j)}(u,q)={\mathsf{map}}_{D(j)}({\mathsf{fold}}_D(\alpha ),u).$$ The unit, constant, and recursive-position cases are reflexivity. Sums and Sigma codes follow the selected branch, and products use both induction hypotheses under pairing. Applying ${\alpha }_j$ to this path gives (80.2). ◻

For lists, the algebra sends the left summand to a chosen $z:X$ and the right summand $(a,x)$ to $c(a,x)$. Expanding (80.2) gives Thus the familiar fold equations are consequences of the code interpretation, not separate axioms.

Proof of Theorem 80.11 — Fold fusion

Proof. Apply description induction to $t={\mathsf{roll}}_j(u)$. Write $f:={\mathsf{fold}}_D(\alpha )$ and $g:={\mathsf{fold}}_D(\beta )$. The induction hypotheses form $$H:{\mathsf{All}}_{D(j)}(\lambda k.\lambda x.{\mathsf{Id}}_{Y(k)}(h_k(f_k(x)),g_k(x)),u).$$ The constructor case is the annotated calculation below. Write (F) for (80.2), (A) for the algebra hypothesis, (M) for map composition from lemma 80.5, and (H) for lemma 80.7 instantiated by the induction hypotheses.  ◻

Proof of Lemma 80.13 — An immediate recursive child is smaller

Proof. Induct on the derivation of $x{◃}_{D(j)}u$. At a recursive-position code, the fold calculation expands the right side to $\mathsf{suc}({\mathsf{size}}_D(x))$. Sums and Sigma codes reduce to the selected branch. At a product, the right side is one plus the sum of the contributions of both components, so the induction hypothesis is preserved by addition of the nonnegative contribution of the other component. These are all clauses of the structurally defined relation. ◻

Proof of Lemma 80.17 — Composite applicative laws

Proof. For composition, expand every composite application and use (80.6) for $F$. Both sides then have the outer forms obtained from $${\mathsf{lift}\mathsf{3}}_F(k,u,v,w):={\mathsf{apply}}_F({\mathsf{apply}}_F({\mathsf{apply}}_F({\mathsf{pure}}_F(k),u),v),w).$$ They are ${\mathsf{lift}\mathsf{3}}_F(k_L,u,v,w)$ and ${\mathsf{lift}\mathsf{3}}_F(k_R,u,v,w)$. For $u_G:G(B\to C)$, $v_G:G(A\to B)$, and $w_G:G(A)$, the two pure functions satisfy Equation (80.6) for $G$ gives their pointwise equality. Three applications of (80.9) give $k_L=k_R$. Congruence under ${\mathsf{pure}}_F$ and the three outer applications therefore gives the composite composition law. The extensionality hypothesis is essential at this step: the unary action law (80.4) does not turn equality after three arguments into equality of the intervening function values.

For identity, put $e_G(x):={\mathsf{apply}}_G({\mathsf{pure}}_G(\mathsf{id}),x)$. Expansion gives the annotated calculation Homomorphism reduces by two instances of (80.7) for $F$ and one for $G$. Interchange expands to two outer $F$ actions; one application of (80.9) turns the pointwise $G$ interchange law into the equality between their pure functions, after which (80.8) for $F$ closes the calculation.

Finally, the homomorphism law for $F$ gives $${\mathsf{map}}_{\mathsf{Comp}(F,G)}(r,u)={\mathsf{map}}_F({\mathsf{map}}_G(r),u).$$ Pointwise equality $r(a)=s(a)$ gives ${\mathsf{map}}_G(r,x)={\mathsf{map}}_G(s,x)$ by extensional action for $G$. Extensional action for $F$ then proves the displayed law for the composite. ◻

Proof of Proposition 80.19 — Traversal laws

Proof. Induct on $D$. For identity, unit, constant, and recursive-position codes reduce by beta computation. Sum and Sigma codes apply their induction hypothesis under the corresponding constructor. At a product, the identity applicative reduces the traversal clause to $$({\mathsf{traverse}}_D(f,u_1),{\mathsf{traverse}}_E(f,u_2)).$$ The two induction hypotheses give the two components required by the product clause of ${\mathsf{map}}_{D\times E}$.

For composition, abbreviate $${\mathsf{lift}\mathsf{2}}_F(k,x,y):={\mathsf{apply}}_F({\mathsf{map}}_F(k,x),y).$$ Let $A_0,A_1,B_0,B_1,C:{\mathcal{U}}_i$, let $x:F(A_0)$ and $y:F(B_0)$, and let $r:A_0\to G(A_1)$, $s:B_0\to G(B_1)$, and $k:A_1\to B_1\to C$. Expansion of the composite application, followed by the composition and homomorphism laws for $F$, gives The only equality between functions in this expansion is obtained from (80.9); its pointwise components are the composition laws for $F$ and $G$ proved in lemma 80.17. In the product case, apply (80.10) with $k:=\mathsf{pair}$. The two induction hypotheses give the pointwise replacements for $r$ and $s$, and (80.4) for $F$ applies them under the outer action. Sum and Sigma codes are the unary instance of the same calculation. Unit, constant, and recursive-position codes reduce to the applicative identity, homomorphism, and composition equations. The code induction has now treated all constructors. ◻

The indexed strictly-positive-family universe

The regular codes above name recursive sorts directly. A genuinely indexed description must also say how constructor data constrain the result index and how recursive arguments are indexed. We now freeze the Morris–Altenkirch–Ghani universe rather than pretending that an arbitrary family of regular codes is already its full syntax.

Let $\overrightarrow{I}=(I_1,\dots ,I_n)$ be a telescope of input-family index types and let $O:{\mathcal{U}}_i$ be the output index. An indexed strictly positive type code $T:\mathsf{ISPT}(\overrightarrow{I})$ has input variables $\mathsf{vz}(i)$ and $\mathsf{vs}(T)$, the codes $\mathsf{0}$ and $\mathsf{1}$, dependent index aggregation ${\mathsf{\Sigma }}_f(F,o^{\prime })$ and ${\mathsf{\Pi }}_f(F,o^{\prime })$, and the fixed-point code $\mu (F,o^{\prime })$. Here $f:O\to O^{\prime }$, $F:O\to \mathsf{ISPT}(\overrightarrow{I})$, and $o^{\prime }:O^{\prime }$ for $\mathrm{\Sigma }$ and $\mathrm{\Pi }$, while a family description is $$\mathsf{SPF}(\overrightarrow{I},O):=O\to \mathsf{ISPT}(\overrightarrow{I}).$$ The syntax is indexed by the complete input telescope; the output index is an argument to a family code, not a meta-level case split hidden from the universe.

For an environment $\rho$ assigning a family to each input variable, the interpretation selects that family at $\mathsf{vz}/\mathsf{vs}$ and has The last line extends $\rho$ by the family being defined before interpreting recursive variables. Its introduction equation is syntactic: $${\mathsf{out}}_{o^{\prime }}({\mathsf{roll}}_{o^{\prime }}(u))\equiv u.$$ The ${\mathrm{\Sigma }}_f$ code chooses one witness whose index maps to $o^{\prime }$; the ${\mathrm{\Pi }}_f$ code stores data at every such witness. These are distinct codes, not abbreviations for ordinary sum and function types outside the universe.

Finite regular sums and products compile into this universe. A Boolean $\mathrm{\Sigma }$ over the constant map into the unique output yields binary choice; finite $\mathrm{\Pi }$ yields a product. A constant payload is a nonrecursive input field, and a regular recursive position is a variable followed by $\mu$. This recovers the Benke–Dybjer–Jansson regular presentation as a bounded derived normal form: it does not replace the principal indexed syntax.

The vector family is now an internal code. Its zero constructor chooses the result index $\mathsf{0}$ and carries unit; its cons constructor chooses $n:\mathbb{N}$, stores $a:A$, requests one recursive child at $n$, and returns $\mathsf{suc}(n)$. In the earlier regular notation its two fibers normalize to Thus ${\mathsf{roll}}_{\mathsf{0}}(\star )$ and ${\mathsf{roll}}_{\mathsf{suc}(n)}((a,xs))$ have exactly the constructor indices of definition 78.1. The displayed normal forms are derived from the index equality stored by ${\mathrm{\Sigma }}_f$; they are not an assertion that every indexed family is an external case split.

Map, fold, traversal, and induction extend by structural recursion on $\mathsf{ISPT}$. At ${\mathrm{\Sigma }}_f$ they preserve the witness and its index equality, and at ${\mathrm{\Pi }}_f$ they act pointwise. At $\mu$ they use the recursive map or fold supplied by the extended environment. The identity/composition and fusion proofs add one congruence case for each constructor. We do not identify these codes with containers: shapes and positions begin in the next chapter.

Induction, equality, and elaboration

Generic equality needs more than strict positivity. The full MAG universe contains ${\mathrm{\Pi }}_f$, hence possibly infinite branching, and its ${\mathrm{\Sigma }}_f$ index witnesses need not have decidable equality. We therefore prove equality only for a smaller finite regular fragment, exactly as the source does.

Proof of Lemma 80.22 — Decidable equality gives local UIP

Proof. Fix $a,b:A$ and put $E_{a,b}:={\mathsf{Id}}_A(a,b)$. Define an endomap $f_{a,b}:E_{a,b}\to E_{a,b}$ by eliminating $d(a,b)$: This endomap is weakly constant. In the positive case both outputs are $r$; in the negative case $n(p):\mathbf{0}$ eliminates to an identification between the outputs. Write the resulting path as ${\kappa }_{a,b}(p,q):f_{a,b}(p)=f_{a,b}(q)$.

Path induction on $p:E_{a,b}$ gives $$p=f_{a,a}(\mathsf{refl}{)}^{-1}\cdot f_{a,b}(p).$$ The reflexivity case is the inverse law from theorem 30.20. For $p,q:E_{a,b}$, write (P) for (80.12) and (K) for ${\mathsf{ap}}_{\lambda r.f_{a,a}(\mathsf{refl}{)}^{-1}\cdot r}({\kappa }_{a,b}(p,q))$. Then Thus the supplied decision procedure gives UIP at this occurrence; no ambient UIP axiom is used. ◻

Proof of Theorem 80.23 — Generic decidable equality

Proof. Define a bounded comparison by ordinary natural-number recursion with the fuel bound in its domain. Here abbreviates $\mathsf{suc}(n)\le m$: $${\mathsf{DecEq}}_A(x,y):={\mathsf{Id}}_A(x,y)+\mathrm{\neg }{\mathsf{Id}}_A(x,y).$$ At zero, the bound implies and eliminates to the required decision. Thus the zero clause does not manufacture a disequality. At a successor, compare the two layers obtained by ${\mathsf{out}}_j$. The completeness invariant is For arbitrary $t,u:\mathsf{Mu}(\lfloor D\rfloor )(j)$, invoke it initially at $$N:={\mathsf{size}}_{\lfloor D\rfloor }(t)+{\mathsf{size}}_{\lfloor D\rfloor }(u)+\mathsf{suc}(\mathsf{0}).$$ The successor clause uses a second recursion on the code. Unit layers agree. Constant positions use the decision stored in $\mathsf{K}(A,d_A)$. A sum first compares its injections; equal injections recurse on their payloads, and unequal injections use disjointness. Products compare the left components and then the right components, combining positive paths by pair congruence and transporting a negative component decision backwards along the corresponding projection. Recursive positions invoke ${\mathsf{eq}}_{\mathsf{pred}(N)}$ on the selected proper subtrees. If $t^{\prime },u^{\prime }$ are those children, two applications of lemma 80.13, followed by addition, give $${\mathsf{size}}_{\lfloor D\rfloor }(t^{\prime })+{\mathsf{size}}_{\lfloor D\rfloor }(u^{\prime })+2\le {\mathsf{size}}_{\lfloor D\rfloor }(t)+{\mathsf{size}}_{\lfloor D\rfloor }(u).$$ Hence (80.14) implies , the completeness hypothesis for the recursive call.

The definition is accepted because it is structurally recursive on $N$; the size inequality proves completeness rather than termination. For soundness, congruence of ${\mathsf{roll}}_j$ turns an accepted layer path into a path between terms. For completeness, apply ${\mathsf{ap}}_{{\mathsf{out}}_j}(-)$ to any path between the two rolls, obtaining a layer path, and then recurse on the code. Products split their path into component paths. Sums use constructor disjointness and injectivity. No dependent tag witness or function-space constructor occurs in this grammar; adding either requires a new coherence or finite-enumerability argument. In particular, lemma 80.22 is not used to enlarge the accepted code fragment. ◻

Let $d_{\mathbb{N}}$ be the usual decision procedure on natural numbers and let $D_{\mathsf{Tree}(\mathbb{N})}^{=}$ be the $\mathsf{EqDesc}$ code obtained from the tree code by storing $d_{\mathbb{N}}$ at its constant position. Its first nontrivial tests expose the sum tag before any recursive call: Here and are the canonical natural-order witnesses, and $n_{\mathsf{tag}}$ is obtained by disjointness of $\mathsf{inl}$ and $\mathsf{inr}$; the rejected comparison does not inspect either subtree.

Proof of Theorem 80.25 — Soundness of the displayed elaboration

Proof. Induct on the constructor list, and inside one constructor induct on its argument telescope. A nonrecursive argument $B$ contributes $\mathsf{K}(B)$ after its source formation derivation establishes $B:{\mathcal{U}}_i$. A recursive argument at index $j$ contributes $\mathsf{X}(j)$ after the result-index premise establishes $j:I$. Products concatenate fields and sums concatenate constructors, preserving well-formedness by the code formation rules. The strict-positivity premise excludes the only unsupported case, a recursive occurrence to the left of an arrow. Finally Mu-intro wraps each interpreted layer. Unfolding the interpretation gives the original constructor telescope, with recursive occurrences replaced by $\mathsf{Mu}(D)$, so each generated $c_i$ has the claimed type. The Tree calculation is the two code clauses displayed in construction 80.24.

This is the local specialization of the soundness shape in Dagand–McBride, Theorem 4 ['EDM12]: their conclusion is validity of the generated declaration after successful elaboration. We have proved it only for the surface grammar and target codes displayed here; no completeness or equivalence with a host language’s inductive declarations follows. ◻

The elaborated code, its fold, its induction principle, and its equality test compose in one bounded derivation: the Tree declaration elaborates to a code, its fold comes from (80.2), its induction principle is definition 80.4, and its equality test uses theorem 80.23 when $A$ has decidable equality. No container representation or row-polymorphic extensibility has entered the argument. Extensible generic datatypes additionally assume decidable labels, row membership, and coherent row permutation; those assumptions are not rules of ${\mathsf{Desc}}_i(I)$.

A binding description

Ordinary descriptions treat every recursive child at the same scope. A lambda body instead lives in a context extended by the bound variable. A regular recursive-position code cannot distinguish these two cases. Binding descriptions repair exactly that defect by storing the telescope introduced above each recursive child.

Let $S:{\mathcal{U}}_i$ be a type of object sorts, let $\mathsf{Ctx}(S)$ be lists of sorts, and let $\mathsf{ext}(\mathrm{\Xi },\mathrm{\Gamma })$ denote the context obtained by placing the finite telescope $\mathrm{\Xi }$ before $\mathrm{\Gamma }$: $$\mathsf{ext}([],\mathrm{\Gamma }):=\mathrm{\Gamma },\mathsf{ext}(B::\mathrm{\Xi },\mathrm{\Gamma }):=B::\mathsf{ext}(\mathrm{\Xi },\mathrm{\Gamma }).$$

Suppose $X$ is scoped over $\mathrm{\Gamma }$ and $Y$ over $\mathrm{\Delta }$. A family $$h_{\mathrm{\Xi },B}:X(\mathsf{ext}(\mathrm{\Xi },\mathrm{\Gamma }),B)\to Y(\mathsf{ext}(\mathrm{\Xi },\mathrm{\Delta }),B)$$ induces ${\mathsf{bmap}}_E(h):{\mathsf{El}}_{\mathrm{\Gamma }}(E,X)\to {\mathsf{El}}_{\mathrm{\Delta }}(E,Y)$ by recursion on $E$. It applies $h_{\mathrm{\Xi },B}$ at $\mathsf{rec}(\mathrm{\Xi },B)$ and follows the remaining code constructors.

Proof of Lemma 80.27 — Binding-layer action laws

Proof. Induct on $E$. At $\mathsf{rec}(\mathrm{\Xi },B)$ the three claims are respectively the identity equation, composition equation, and pointwise path. Unit and constants give reflexivity. Sums follow their injection, products use the two induction hypotheses, and Sigma codes retain their tag and use the branch induction hypothesis. These cases prove all three laws. ◻

Take $V(\mathrm{\Gamma },A):=\mathsf{Var}(\mathrm{\Gamma },A)$, the intrinsically typed de Bruijn variables. For $B:S$, their newest and older constructors have types $$\mathsf{vz}:\mathsf{Var}(B::\mathrm{\Gamma },B),\mathsf{vs}:\mathsf{Var}(\mathrm{\Gamma },A)\to \mathsf{Var}(B::\mathrm{\Gamma },A).$$ Define A renaming lifts through a telescope $\mathrm{\Xi }$. For one new sort $B$, let ${\mathsf{wk}}_B^{\mathrm{\Gamma }}(x):=\mathsf{vs}(x)$ and define Put $${\mathsf{lift}}_{[]}(\rho ):=\rho ,{\mathsf{lift}}_{B::\mathrm{\Xi }}(\rho ):={\mathsf{lift}}_{[B]}({\mathsf{lift}}_{\mathrm{\Xi }}(\rho )).$$

Free-syntax induction defines generic renaming: A substitution lift may now use this renaming. Define Put $${\mathsf{lift}}_{[]}(\sigma ):=\sigma ,{\mathsf{lift}}_{B::\mathrm{\Xi }}(\sigma ):={\mathsf{lift}}_{[B]}({\mathsf{lift}}_{\mathrm{\Xi }}(\sigma )).$$ Thus every newly introduced variable is fixed, and every older image is weakened through the whole telescope. Free-syntax induction then defines generic substitution: Every context change occurs at the recursive-position clause that names its telescope.

Proof of Theorem 80.28 — Generic renaming and substitution laws

Proof. The proof is staged because lift compatibility for substitution composition uses both mixed laws on arbitrary substitution images.

First prove renaming congruence, identity, and composition by free-syntax induction. Variable cases are the corresponding environment paths. For a constructor $\mathsf{con}(u)$, the recursive-position premises of lemma 80.27 are the induction hypotheses. Induction on $\mathrm{\Xi }$ and variable elimination give where $e\sim e^{\prime }$ means pointwise equality. A newest variable gives reflexivity; an older variable reduces the second line to $\mathsf{vs}(\tau (\rho (x)))=\mathsf{vs}(\tau (\rho (x)))$.

Next prove substitution congruence and identity by the same syntax induction. The older-variable clause of the lifted identity is $${\mathsf{ren}}_F({\mathsf{wk}}_B^{\mathrm{\Gamma }},\mathsf{var}(x))\equiv \mathsf{var}(\mathsf{vs}(x)).$$ Prove substitution after renaming next. At an older variable, preservation of $\mathsf{rsub}$ is definitional. Abbreviate $\hat{\sigma }:={\mathsf{lift}}_{[B]}(\sigma )$ and $\hat{\rho }:={\mathsf{lift}}_{[B]}(\rho )$. Then $$\mathsf{rsub}(\hat{\sigma },\hat{\rho })(\mathsf{vs}(x))\equiv {\mathsf{ren}}_F({\mathsf{wk}}_B^{\mathrm{\Theta }},\sigma (\rho (x)))\equiv {\mathsf{lift}}_{[B]}(\mathsf{rsub}(\sigma ,\rho ))(\mathsf{vs}(x)).$$

Renaming after substitution follows by syntax induction using the renaming composition law already proved. Its older-variable lift comparison is

It remains to prove substitution composition. The newest-variable lift case is reflexivity. At an older variable, the two mixed laws give Induction on $\mathrm{\Xi }$ iterates each one-sort comparison. Binding-layer congruence converts the resulting pointwise lift paths into constructor paths. At no stage is an equality between environment functions used. ◻

Let ${\mathsf{wk}}_B^{\mathrm{\Gamma }}:\mathsf{Ren}(\mathrm{\Gamma },B::\mathrm{\Gamma })$ be the inclusion. For $\tau :{\mathsf{Sub}}_F(\mathrm{\Gamma },\mathrm{\Delta })$ and $t:{\mathsf{Tm}}_F(V;\mathrm{\Gamma },A)$, the final equation of theorem 80.28, followed by the substitution-after-renaming equation, gives the naturality law $${\mathsf{ren}}_F({\mathsf{wk}}_B^{\mathrm{\Delta }},{\mathsf{sub}}_F(\tau ,t))={\mathsf{sub}}_F({\mathsf{lift}}_{[B]}(\tau ),{\mathsf{ren}}_F({\mathsf{wk}}_B^{\mathrm{\Gamma }},t)).$$ Indeed, both sides are substitutions into $t$. On a variable $x$ their environments reduce to ${\mathsf{ren}}_F({\mathsf{wk}}_B^{\mathrm{\Delta }},\tau (x))$; generic environment congruence proves the displayed equality. The same derivation applies in an extended context because the theorem quantifies over arbitrary source and target contexts.

For simply typed lambda terms, take $S:=\mathsf{Ty}$, generated by $o$ and arrows, and define Write $\mathsf{Tm}(\mathrm{\Gamma },A)$ for ${\mathsf{Tm}}_{F_{\lambda }}(\mathsf{Var};\mathrm{\Gamma },A)$. The two constructor summands are $\mathsf{app}$ and $\mathsf{lam}$. The generic equations become

The four concrete representations in chapter 23 instantiate different boundaries of this theorem. Typed de Bruijn syntax is the displayed $\mathsf{Var}$ instance. Locally nameless syntax changes the variable family but retains telescope lifting. PHOAS replaces environments by a parametric host family, so its exclusion of exotic terms still requires the parametricity theorem proved there. Contextual syntax exposes $\mathrm{\Gamma }$ in open terms and substitutions. The generic theorem gives the common scope-safe traversal and fusion argument; it does not give LF adequacy, nominal freshness, or PHOAS parametricity.

Suggested first pass.

Begin with exercise 80.6, exercise 80.7.

Exercise 80.6¶

★★☆ For binary trees, define a mirror algebra and a node-counting algebra. Use theorem 80.11 to prove that node count is invariant under mirror. Expand the algebra-commuting hypothesis in the leaf and fork summands.

Referenced from 4 locations

• Universes of Datatype Descriptions and Generic Programs
• ch:datatype-descriptions: ch:datatype-descriptions

Exercise 80.7¶

★★☆ Reconstruct the renaming-after-substitution equation of theorem 80.28 at a constructor $\mathsf{con}(u)$. State the recursive-position premise supplied by lemma 80.27. Then specialize it to the $\mathsf{lam}$ constructor, where the stored telescope is $[B]$.

Referenced from 4 locations

• Universes of Datatype Descriptions and Generic Programs
• ch:datatype-descriptions: ch:datatype-descriptions

Exercise 80.8¶

★★☆ Run the bounded equality procedure on the two layers $(\mathsf{false},\star )$ and $(\mathsf{true},(l,r))$ of $D_{\mathsf{Tagged}}$. Identify the first rejected comparison. Then remove the decision procedure for $\mathbf{2}$ from the Sigma equality data and state the exact algorithmic clause that can no longer be executed.

Referenced from 3 locations

• Universes of Datatype Descriptions and Generic Programs
• ch:datatype-descriptions: ch:datatype-descriptions

Exercise 80.9¶

★★★ Practical project.generic-description-interpreter Implement in Kappa the six constructors of ${\mathsf{Desc}}_i(I)$, their interpretation for regular codes, $\mathsf{roll}$, generic map, fold, and size. Maintain the invariant that every recursive position is interpreted by the family parameter and no negative occurrence is accepted. Elaborate the displayed Tree declaration, construct $\mathsf{fork}(\mathsf{leaf}(1),\mathsf{leaf}(2))$, and produce size $3$ and the leaf list $[1,2]$. Represent the Boolean-indexed instance of $\mathsf{sigma}$ by a tag-to-code lookup, and test that its false tag accepts a unit payload while its true tag accepts a pair of recursive payloads; both crossed payload shapes must be rejected. The acceptance test must also reject a declaration with constructor argument $\mathsf{Tree}(A)\to A$, reporting a negative recursive occurrence.

Referenced from 4 locations

• Universes of Datatype Descriptions and Generic Programs
• Object calculus checker and evaluator
• ch:datatype-descriptions: ch:datatype-descriptions