Typed Self-Representation in System F-omega

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

Typed self-representation without a paradox $\star$

Strong normalization appears to forbid a self-interpreter. An interpreter which can consume its own text seems to invite the same diagonal argument which proves that there is no total computable universal function for the total computable functions. The conclusion is too quick. The diagonal argument needs one particular self-application to be well typed, and a typed representation is indexed precisely so that this application need not be well typed.

The diagonal step that typing refuses

Let us recall the classical argument in the form that matters here. Suppose that a total computable function $$\mathcal{U}:\mathbb{N}\times \mathbb{N}⟶\mathbb{N}$$ were universal for total computable unary functions: for every such function $f$ there would be an index $a$ with $f(n)=\mathcal{U}(a,n)$ for all $n$. Then $$d(n):=\mathcal{U}(n,n)+1$$ would itself be total and computable. If $a$ indexed $d$, then $d(a)=\mathcal{U}(a,a)+1=d(a)+1$, a contradiction. The two occurrences of $a$ in $\mathcal{U}(a,a)$ are the whole mechanism.

Here is the corresponding calculation for terms. A quotation is provisionally the result of an external operation on a chosen closed typing derivation $\mathcal{D}:e:A$; write its result as $\hat{\mathcal{D}}$, or temporarily as $\hat{e}$ when the derivation is fixed. Suppose that a closed internal term $u$ unquotes every genuine quotation: $$u\hat{e}{=}_{\beta }e.$$ Suppressing annotations for the moment, form $$p_u:=\lambda x.\lambda y.(ux)x.$$ The vacuous binder $\lambda y$ plays the role of the classical $+1$: it makes the diagonal reduct differ from itself by exactly one abstraction node. If $\widehat{p_u}$ exists and the diagonal application $p_u\widehat{p_u}$ is typable, then The equation looks paradoxical, but only after the italicized typing assumption has been made.

The barrier argument needs unique normal forms for a relation that also normalizes constructor annotations. Let ${⟹}_{\beta }$ be the compatible closure, through a term, of term beta contraction and constructor beta contraction in annotations and type arguments. Write ${\equiv }_{\beta }^{\mathrm{m}\mathrm{i}\mathrm{x}}$ for its symmetric, transitive closure. To obtain unique normal forms, it remains to prove that two reductions from one term can be joined. Root and congruence reduction overlap at beta-redexes, so the joining relation must commute with both term and constructor substitution.

Proof of Lemma 17.1 — Mixed parallel substitution and diamond

Proof. The first substitution law is the induction of lemma 5.37; its abstraction case additionally uses constructor congruence on the binder annotation. Prove the second by induction on $e{\Rrightarrow }_{\mathrm{m}}{e}^{\prime }$. Constructor annotations and type arguments use constructor substitution. In the term-beta case, constructor substitution commutes with capture-avoiding term substitution. The only new root calculation is type beta. Alpha-rename its binder $v$ so that $v\notin \{u\}\cup \mathrm{FV}(C)\cup \mathrm{FV}(C^{\prime })$. The two orders are identified by $$e_0[D/v][C/u]=e_0[C/u][D[C/u]/v],$$ and the induction hypotheses reduce both sides in parallel to

$$e_0^{\prime }[D^{\prime }/v][C^{\prime }/u]=e_0^{\prime }[C^{\prime }/u][D^{\prime }[C^{\prime }/u]/v].$$

For the diamonds, use the source-form complete development. Its complete term clauses are where the two application clauses and the two type-application clauses are selected by the source outer form. An annotation or type argument is developed by constructor complete development, whose complete clauses are The last clause applies when $A$ is not syntactically a constructor abstraction. These clauses are exhaustive for the displayed term and constructor grammars. In particular, constructor application contracts only a source of the displayed beta form and otherwise develops the two components without contracting their result. Thus development does not contract a redex created by developing an immediate component. Induction on a parallel derivation shows that every parallel reduct takes one further parallel step to this complete development. For application congruence, split on the source outer form of $e_1$. If $e_1$ is not an abstraction, from $e_i{\Rrightarrow }_{\mathrm{m}}{e}_i^{\prime }$ the induction hypotheses give $e_i^{\prime }{\Rrightarrow }_{\mathrm{m}}{e}_i^{\bullet }$, hence $e_1^{\prime }{e}_2^{\prime }{\Rrightarrow }_{\mathrm{m}}{e}_1^{\bullet }{e}_2^{\bullet }$, the complete development. If $e_1=\lambda x:A.b$, then $e_1^{\prime }=\lambda x:A^{\prime }.b^{\prime }$ for parallel reducts $A^{\prime },b^{\prime }$. Apply the root clause to $e_1^{\prime }{e}_2^{\prime }$ and the substitution law to reach $b^{\bullet }[e_2^{\bullet }/x]$, the complete development of the source application. A constructor root–congruence overlap at $(\lambda u.A)C$ joins at $A^{\bullet }[C^{\bullet }/u]$ by constructor substitution. A term root–congruence overlap at $(\lambda x:A.e)d$ joins at $e^{\bullet }[d^{\bullet }/x]$ by the first displayed law. Finally, the new overlap at $(\mathrm{\Lambda }u::\kappa .e)[C]$ joins at $e^{\bullet }[C^{\bullet }/u]$ by the second law. These are the only root overlaps. Thus every parallel reduct of $a$ takes one parallel step to $a^{\bullet }$. Fix either of the two parallel relations. If $a$ reduces in parallel to both $b$ and $c$, then both $b$ and $c$ reduce in parallel to $a^{\bullet }$. This proves the diamond property for each relation. ◻

Proof of Lemma 7.56 — Term normalization and confluence used here

Proof. The source proves strong normalization of every well-typed term in the pure $F_{\omega }$ signature under combined beta reduction [Bar92]. This relation contracts both term-level and constructor-level beta redexes; on the separated syntax printed here it is exactly ${⟹}_{\beta }$. The term-only relation is a subrelation. Expanding a named abbreviation adds no reduction rule.

By lemma 17.1, mixed parallel reduction is diamond. Every mixed one-step contraction is parallel, and every parallel step can be serialized into finitely many compatible mixed steps, by induction on its derivation. The path-length argument of theorem 5.38 therefore gives mixed confluence. Restricting the parallel clauses to term roots and holding annotations and type arguments fixed gives term-only confluence. ◻

Proof of Proposition 7.57 — The normalization barrier, exactly stated

Proof. Fix either relation from the statement. Assume that the application is well typed. Its first term-beta reduct is well typed by subject reduction. The unquoting hypothesis relates $u\widehat{p_u}$ to $p_u$ in the chosen relation. Compatible congruence under application and abstraction therefore relates $\lambda y.(u\widehat{p_u})\widehat{p_u}$ to $\lambda y.p_u\widehat{p_u}$; this is the second step of (7.6).

By lemma 7.56, let $v$ be the normal form of $p_u\widehat{p_u}$ in the chosen relation. Confluence says that equivalent well-typed terms have alpha-equivalent normal forms. Compatible reduction under the outer abstraction gives $\lambda y.v$ as the normal form of the last term in (7.6). Hence $v$ would be alpha-equivalent to $\lambda y.v$. This is impossible: the latter finite syntax tree contains one more abstraction node. Therefore the diagonal application is not well typed. ◻

The proposition does not say that $u$ is untypable. It does not even say that $p_u$ is untypable. It says that the represented type attached to $\widehat{p_u}$ does not permit the second use of the same argument required by the diagonal. This is the point at which the analogy with one untyped universal domain ends.

The proposition is conditional. Its antecedent is not a property of the deep indexed representation. Its unquoter has type $$\mathsf{unquote}:\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{Op}\mathsf{Id}\alpha .$$ Under $\alpha ::U$ and $x:\mathsf{Exp}\alpha$, the attempted body $(\mathsf{unquote}[\alpha ]x)x$ would require constructor conversion $$\mathsf{Op}\mathsf{Id}\alpha {=}_{\beta }\mathsf{Exp}\alpha \to B$$ for some $B$. Unfolding $\mathsf{Op}$ gives the two contractions $$\mathsf{Op}\mathsf{Id}\alpha {⇝}_0\mathsf{Id}(\alpha \mathsf{Id}){⇝}_0\alpha \mathsf{Id}.$$ The result has neutral constructor head $\alpha$, so its constructor normal form cannot have arrow head. Strong normalization and unique constructor normal forms theorem 7.21, corollary 7.24 reject the application before any term reduction occurs. At a genuine closed index $\alpha =\hat{A}$, the same result type reduces to $A$, which is exactly why ordinary unquotation remains typable. Here and until the formal construction below, $\hat{A}$ denotes a constructor of kind $U$; it is distinct from the term quotation $\hat{e}$.

The pure calculus

Quotation and unquotation use the pure $F_{\omega }$ fragment generated by with the kinding and typing rules of chapter 9. Constructor conversion is type-level beta conversion. Compatible term reduction has the two root contractions $$(\lambda x:A.e_1)e_2{⟶}_{\beta }{e}_1[e_2/x],(\mathrm{\Lambda }u::\kappa .e)[C]{⟶}_{\beta }e[C/u]$$ and is closed under binders and both operands of an application. A term is normal when its term tree contains neither root; constructor redexes in type annotations and type arguments do not affect this predicate.

Write $e{\approx }_{\mathrm{t}\mathrm{y}}{e}^{\prime }$ when $e$ and $e^{\prime }$ have the same term tree and corresponding constructor components are beta-convertible. For the term-only closure ${⟶}_{\beta }^{\ast }$ and the mixed reduction ${⟹}_{\beta }$ fixed before lemma 17.1, $$e{⟶}_{\beta }^{\ast }{e}^{\prime }⟹e{⟹}_{\beta }^{\ast }{e}^{\prime },e{\approx }_{\mathrm{t}\mathrm{y}}{e}^{\prime }⟹e{\equiv }_{\beta }^{\mathrm{m}\mathrm{i}\mathrm{x}}{e}^{\prime }.$$ Deep unquotation reduces by ${⟹}_{\beta }^{\ast }$ to the source term. Restricting the calculation to ${⟶}_{\beta }$ instead yields some $e^{\prime }$ with $e^{\prime }{\approx }_{\mathrm{t}\mathrm{y}}e$: constructor normalization may change annotations, but not the term tree or its normality.

Names such as $\mathsf{Bool}$ and $\mathsf{Nat}$ abbreviate the Church encodings ${\mathsf{Bool}}_F$ and ${\mathsf{Nat}}_F$ of definition 5.15, definition 5.18, with explicit kind annotations. Every named declaration in this chapter expands to one term of the stated grammar. A constructor binder without an explicit kind in a program formula has kind $\mathsf{Ty}$; term binders retain their type annotations.

A shallow representation

The quotation must be beta-normal while substituting a fixed identity must recover the source. Copying the source under a fresh binder does not meet the first requirement: for the redex $(\lambda x:A.x)y$, the naive candidate $$\lambda i:I.(\lambda x:A.x)y$$ still contains that redex. The repair is to record each application under an inert variable head, so that the application node becomes stuck until unquotation replaces the inert variable by the identity. Put $$I:=\mathrm{\forall }Z::\mathsf{Ty}.Z\to Z,i:I.$$ The letter $i$ is a fresh, designated term variable. Quotation is defined on a typing derivation, rather than on an unannotated term, because an application node must record the function type found by that derivation.

The application clauses are easy to read by calculation. Since $i$ is a variable, $$i[A\to B]q_1{q}_2\text{and}i[\mathrm{\forall }u::\kappa .A]q[C]$$ are stuck, hence normal, yet replacing $i$ by the polymorphic identity erases the inserted node in either case.

Proof of Lemma 7.59 — Typing and normality of shallow quotation

Proof. Induct on the typing derivation. The variable, term-abstraction, and type-abstraction cases use the same typing rule as the source derivation and the induction hypothesis for the immediate premise.

For term application the two induction hypotheses give $q_1:A\to B$ and $q_2:A$. The variable $i$ has the instances $$i[A\to B]:(A\to B)\to (A\to B),i[A\to B]q_1:A\to B,$$ so $i[A\to B]q_1{q}_2:B$. For type application the induction hypothesis gives $q:\mathrm{\forall }u::\kappa .A$, and $$i[\mathrm{\forall }u::\kappa .A]q:\mathrm{\forall }u::\kappa .A;$$ applying this term to $C$ gives $A[C/u]$. A final conversion changes only the claimed result type.

Now assume the derivation closed. Abstracting $i$ gives type $I\to A$. For normality, induct once more over the same clauses. A copied abstraction cannot introduce a redex. At either application clause the head is the variable $i$, not an abstraction; the induction hypotheses say that all proper term subexpressions are normal. The conversion case changes no term. For a term abstraction $\mathrm{\Gamma },x:A⊢e:B$, the body induction hypothesis holds under $x:A$; copying the binder therefore gives type $A\to B$ without introducing a redex. ◻

Define the closed polymorphic identity and the internal shallow unquoter by Unlike quotation, this is an ordinary term of $F_{\omega }$.

Proof of Theorem 7.60 — Strong shallow unquoting

Proof. After the outer type contraction and two term contractions it is enough to prove the stronger assertion $$\begin{array}{}\text{(}†\text{)}& q[{\mathsf{id}}_I/i]{⟶}_{\beta }^{\ast }e\end{array}$$ for every shallow prequotation. We induct on its typing derivation. A variable is unchanged. Term and type abstractions follow by compatible reduction under the binder and the corresponding induction hypothesis.

For term application, the decisive part of the calculation is $${\mathsf{id}}_I[A\to B]q_1^{\prime }{q}_2^{\prime }{⟶}_{\beta }^{\ast }{q}_1^{\prime }{q}_2^{\prime }{⟶}_{\beta }^{\ast }{e}_1{e}_2,$$ where $q_j^{\prime }=q_j[{\mathsf{id}}_I/i]$ and the last reductions are the two induction hypotheses. Type application calculates $${\mathsf{id}}_I[\mathrm{\forall }u::\kappa .A]q^{\prime }[C]{⟶}_{\beta }^{\ast }{q}^{\prime }[C]{⟶}_{\beta }^{\ast }e[C].$$ A final conversion added no syntax, so it uses the induction hypothesis unchanged. This proves $(†)$ and hence the theorem. ◻

The shallow construction already breaks through the normalization barrier: the unquoter terminates and returns the represented term. It is too opaque for a size function, however. Its interface exposes no constructor tag or case operator: a consumer can only apply the stored polymorphic term at a chosen result type. A direct inspection of beta-eta normal forms therefore offers no branch that can count the source constructor. To inspect the four term constructors we must expose four cases in the representation itself.

Representing types only as far as the fold needs

Fix a fresh constructor variable $F::\mathsf{Ty}\to \mathsf{Ty}$. Marking every constructor production is too strong. For constructor application it would give $${\mathsf{pre}}_F^{\mathrm{all}}(AB)=F({\mathsf{pre}}_F^{\mathrm{all}}(A){\mathsf{pre}}_F^{\mathrm{all}}(B)),$$ but the argument of the outer $F$ must already have kind $\mathsf{Ty}$, whereas $A$ may have an arrow kind; the application case of the formation induction cannot be rebuilt. Constructor variables, abstractions, and applications must retain their kind, while the arrow and universal productions receive the marker. The $F$-pre-representation of a constructor is defined structurally: the constructor translation ${\mathsf{pre}}_F(A)$ is a syntactic constructor of representation kind. A semantic interpretation such as $[[A{]]}_{\rho }$ instead maps a type to a relation. They are different constructions, and no theorem identifying them is asserted here. The full representation of a closed constructor is $$\hat{A}:=\lambda F::\mathsf{Ty}\to \mathsf{Ty}.{\mathsf{pre}}_F(A).$$ Here $\hat{A}$ is a constructor of kind $U$. By contrast, $\hat{\mathcal{D}}$ is a term quotation determined by the typing derivation $\mathcal{D}$, and $\hat{e}$ abbreviates that term only after its derivation has been fixed. The hat records representation in each case, while the sort of its operand determines whether the result is a constructor or a term. Notice the asymmetry in (7.7). An arrow or universal type classifies terms and is therefore marked by $F$; a constructor variable, constructor abstraction, or constructor application is represented by itself. This is enough information to calculate the result type of each operation; it is not an inductive syntax tree for types.

Proof of Lemma 7.61 — Formation and substitution of type pre-representations

Proof. For (1), induct on the kinding derivation. A variable is unchanged. In an arrow, the induction hypotheses give ${\mathsf{pre}}_F(A),{\mathsf{pre}}_F(B)::\mathsf{Ty}$; applying $F$ to each gives two types and hence their arrow is a type. In a universal, the body hypothesis gives ${\mathsf{pre}}_F(A)::\mathsf{Ty}$ under $u::\kappa$, so $F{\mathsf{pre}}_F(A)::\mathsf{Ty}$ and the universal is formed. Constructor abstraction and application use their two kinding rules directly. Thus variables, arrows, universals, constructor abstractions, and constructor applications each preserve kind $\mathsf{Ty}$ under prequotation.

For (2), induct on $A$. For an arrow, $${\mathsf{pre}}_F((A\to B)[C/u])=F{\mathsf{pre}}_F(A[C/u])\to F{\mathsf{pre}}_F(B[C/u]),$$ and the two induction hypotheses rewrite this to $${\mathsf{pre}}_F(A\to B)[{\mathsf{pre}}_F(C)/u].$$ Variables and applications are homomorphic. Under either binder, first rename its bound variable away from $u$ and the free variables of $C$, then apply the induction hypothesis to the body. This accounts for both constructor abstraction and universal quantification.

For (3), it suffices by congruence to inspect one constructor beta step. By (2), The conclusion about $\hat{A}$ is now one use of constructor abstraction. ◻

Type application creates a difficulty that did not occur in the shallow representation. If $e:\mathrm{\forall }u::\kappa .A$, its representation has to remember how to obtain the instance at $C$. We record that relationship extensionally by the ordinary term $${\mathsf{inst}}_{P,Q}:=\lambda x:P.x[Q]:P\to B[Q/u],P=\mathrm{\forall }u::\kappa .B,Q::\kappa .$$ The notation is defined only when $P$ has the displayed universal form and $Q$ has the displayed kind. It is not a kind-polymorphic $F_{\omega }$ function; each occurrence in a quotation is a separately constructed term.

Type abstraction creates the dual difficulty. Its body has a redundant quantifier after the constant-result folds used by $\mathsf{size}$ and $\mathsf{isNormal}$. Concretely, under a constant fold $K_X=\lambda A.X$, the recursive value has type $x:\mathrm{\forall }u::\kappa .X$, while the case branch must return $X$. It suffices to instantiate $x$ at one fixed constructor of kind $\kappa$. The type $\mathsf{Strip}$ records this operation uniformly. Every kind has such a closed constructor: $$S_{\mathsf{Ty}}:=\mathrm{\forall }X::\mathsf{Ty}.X,S_{{\kappa }_1\to {\kappa }_2}:=\lambda u::{\kappa }_1.S_{{\kappa }_2}.$$ The kinding judgment $⊢S_{\kappa }::\kappa$ follows by induction on $\kappa$. At the base kind the concrete calculation is one use of K-All: $$X::\mathsf{Ty}⊢X::\mathsf{Ty}⟹⊢\mathrm{\forall }X::\mathsf{Ty}.X::\mathsf{Ty}.$$ For the arrow step, the induction hypothesis gives $⊢S_{{\kappa }_2}::{\kappa }_2$; weakening places it under $u::{\kappa }_1$, and K-Abs derives $⊢\lambda u::{\kappa }_1.S_{{\kappa }_2}::{\kappa }_1\to {\kappa }_2$. This claims a closed constructor of kind $\mathsf{Ty}$, not a closed term inhabiting that type. Put $$\mathsf{Strip}:=\lambda F::\mathsf{Ty}\to \mathsf{Ty}.\lambda A::\mathsf{Ty}.\mathrm{\forall }B::\mathsf{Ty}.(\mathrm{\forall }C::\mathsf{Ty}.FC\to B)\to A\to B.$$ If $T::\kappa \to \mathsf{Ty}$, define Then $${\mathsf{strip}}_{F,\kappa ,T}:\mathsf{Strip}F(\mathrm{\forall }u::\kappa .F(Tu)).$$ Indeed, $x[S_{\kappa }]:F(T{S}_{\kappa })$ and $c[T{S}_{\kappa }]:F(T{S}_{\kappa })\to B$. This two-line derivation is the reason for the otherwise arbitrary-looking inhabitant $S_{\kappa }$.

For later calculations record what stripping does when $F$ is the constant function $K_X:=\lambda A::\mathsf{Ty}.X$ and the combining map is the identity: Thus stripping does not erase an arbitrary quantified value. It chooses one well-kinded instance. This is sufficient only when the operation’s answer is independent of type arguments, as size and normality are.

The deep representation and its fold

The naive type-abstraction case would quantify over the represented binder’s kind: $$\mathrm{\forall }\kappa .(\mathrm{\forall }u::\kappa .F(Tu))\to F(\mathrm{\forall }u::\kappa .Tu).$$ This is not a constructor of pure $F_{\omega }$: kinds are not first-class and there is no $\mathrm{\forall }\kappa$. The case type must instead work for each fixed metalevel kind $\kappa$, and receive the uniform stripping operation that extracts a representative body at that kind. The same obstruction determines the type-application case. The repair assigns one case type to each syntactic constructor, recording the represented source and target types in its indices: The binders $P,Q$ in these case types range over represented result constructors; source types are written $A,B$ only in the prequotation clauses of definition 7.62. The fold consumes one algebra component for each representation constructor and returns the component indexed by the represented type. In particular, an application node consumes $\mathsf{App}F$, a represented function in $F(FP\to FQ)$, and a represented argument in $FP$, producing $FQ$. For $\mathsf{TAbs}$, the case consumes the stripping operation and the stripped body $P$, then returns $FP$. In a prequotation, $F$ and the four term variables $\mathit{abs},\mathit{app},\mathit{tabs},\mathit{tapp}$ are fixed. Transform a source context $\mathrm{\Gamma }=x_1:A_1,\dots ,x_n:A_n$ into $${\mathrm{\Gamma }}^F=x_1:F{\mathsf{pre}}_F(A_1),\dots ,x_n:F{\mathsf{pre}}_F(A_n).$$ Abbreviate the complete case-variable context by $${\mathrm{\Xi }}_F:=\mathit{abs}:\mathsf{Abs}F,\mathit{app}:\mathsf{App}F,\mathit{tabs}:\mathsf{TAbs}F,\mathit{tapp}:\mathsf{TApp}F.$$

For a source instance $e[C]$, the recursive quotation has type $FP$, where $P$ represents the universal type of $e$. The instantiation term has type $P\to FR$, where $R$ represents the result type. Therefore the case must accept $FP$, then $P\to FR$, and return $FR$: $$\mathit{tapp}[P]q[R]g:FR(q:FP,g:P\to FR).$$ Accordingly, the $\mathsf{TApp}$ component in (7.11) has type $\mathrm{\forall }P.FP\to \mathrm{\forall }R.(P\to FR)\to FR$; its quantifiers make one case term applicable at every source operator and result type.

Proof of Lemma 7.64 — Fundamental typing lemma for deep quotation

Proof. Induct on $\mathcal{D}$. The variable case is the definition of ${\mathrm{\Gamma }}^F$. For term abstraction the induction hypothesis gives $q:F{\mathsf{pre}}_F(B)$ under $x:F{\mathsf{pre}}_F(A)$. Hence the copied abstraction has type $$F{\mathsf{pre}}_F(A)\to F{\mathsf{pre}}_F(B),$$ and the $\mathit{abs}$ case returns $F(F{\mathsf{pre}}_F(A)\to F{\mathsf{pre}}_F(B))=F{\mathsf{pre}}_F(A\to B)$. For term application, the two induction hypotheses have exactly the first two argument types required by $\mathit{app}$, which returns $F{\mathsf{pre}}_F(B)$.

For type abstraction put $$P:={\mathsf{pre}}_F(\mathrm{\forall }u::\kappa .A)=\mathrm{\forall }u::\kappa .F{\mathsf{pre}}_F(A),T:={\mathsf{pre}}_F(\lambda u::\kappa .A).$$ The induction hypothesis gives $\mathrm{\Lambda }u::\kappa .q:P$, while (7.9) gives ${\mathsf{strip}}_{F,\kappa ,T}:\mathsf{Strip}F(\mathrm{\forall }u::\kappa .F(Tu))$. Since $Tu{\to }_{\beta }{\mathsf{pre}}_F(A)$, constructor conversion changes this type to $\mathsf{Strip}FP$. Thus $\mathit{tabs}[P]$ returns $FP$, as required.

For type application put $P={\mathsf{pre}}_F(\mathrm{\forall }u::\kappa .A)$ and $R={\mathsf{pre}}_F(A[C/u])$. The induction hypothesis gives $q:FP$. By (7.8), ${\mathsf{inst}}_{P,{\mathsf{pre}}_F(C)}$ has domain $P$ and codomain $$(F{\mathsf{pre}}_F(A))[{\mathsf{pre}}_F(C)/u]=F({\mathsf{pre}}_F(A)[{\mathsf{pre}}_F(C)/u])\stackrel{lemma7.61.2}{=}FR.$$ These are exactly the arguments expected by $\mathit{tapp}[P]q[R]$, so the result has type $FR$. In the conversion case, lemma 7.61 converts the induction-hypothesis type to the required one.

For a closed derivation, abstracting the five designated variables yields $$\mathrm{\forall }F::\mathsf{Ty}\to \mathsf{Ty}.\mathsf{Abs}F\to \mathsf{App}F\to \mathsf{TAbs}F\to \mathsf{TApp}F\to F{\mathsf{pre}}_F(A),$$ which is definitionally $\mathsf{Exp}\hat{A}$. Normality follows by the same induction. Every apparent application in $q$ has one of the four case variables at its head. The inserted $\mathsf{inst}$ and $\mathsf{strip}$ terms are themselves normal and are passed as arguments, not applied there. Copied binders preserve normality. Type-level redexes in annotations are, by our convention, not term redexes. ◻

The representation is deep: eliminating a quoted expression requires handlers for term abstraction, term application, constructor abstraction, and constructor application. Applying a quotation to those four handlers is the eliminator of type

Proof of Lemma 7.65 — Fold calculation

Proof. Writing the four case arguments as $a,p,t_a,t_p$, expansion gives the complete head calculation No induction is needed: this is the beta law of the Church encoding, in the sense explained for Church naturals in definition 5.18. ◻

The internal unquoter

Take the identity type operator $$\mathsf{Id}:=\lambda A::\mathsf{Ty}.A$$ and the following four cases: They have types $\mathsf{Abs}\mathsf{Id}$, $\mathsf{App}\mathsf{Id}$, $\mathsf{TAbs}\mathsf{Id}$, and $\mathsf{TApp}\mathsf{Id}$ respectively. Define the ordinary internal $F_{\omega }$ term

Proof of Lemma 7.66 — Recovery of represented types

Proof. Induct on $A$. A variable is unchanged. For an arrow, the induction hypotheses and the two contractions $\mathsf{Id}X{\to }_{\beta }X$ give $$\mathsf{Id}{\mathsf{pre}}_{\mathsf{Id}}(A){\to }_{\beta }^{\ast }A,\mathsf{Id}{\mathsf{pre}}_{\mathsf{Id}}(B){\to }_{\beta }^{\ast }B.$$ For a universal, contract its one occurrence of $\mathsf{Id}$ and reduce under the binder. Constructor abstraction reduces under its binder, and constructor application uses the two induction hypotheses in its operator and argument positions. Hence the variable, arrow, universal, constructor- abstraction, and constructor-application clauses all reduce to their original types under $\mathsf{Id}$.

Finally,  ◻

Proof of Lemma 7.67 — Unquoting a prequotation

Proof. Induct on $\mathcal{D}$. A variable is unchanged. In the term-abstraction case, the $\mathsf{unAbs}$ case contracts to the copied abstraction, and the induction hypothesis reduces its body: $$\mathsf{unAbs}[{\mathsf{pre}}_{\mathsf{Id}}(A)][{\mathsf{pre}}_{\mathsf{Id}}(B)](\lambda x:\mathsf{Id}{\mathsf{pre}}_{\mathsf{Id}}(A).q^{\prime })\stackrel{unfold\mathsf{unAbs},thenbeta}{{⟹}_{\beta }^{\ast }}\lambda x:A.e.$$ By lemma 7.66, $\mathsf{Id}{\mathsf{pre}}_{\mathsf{Id}}(A){\to }_{\beta }^{\ast }A$ and $\mathsf{Id}{\mathsf{pre}}_{\mathsf{Id}}(B){\to }_{\beta }^{\ast }B$, so constructor conversion validates the annotations in this calculation. In term application, $\mathsf{unApp}$ applies the two induction-hypothesis results and hence reduces to $e_1{e}_2$.

In type abstraction, $\mathsf{unTAbs}$ ignores its strip argument and returns the copied type abstraction; compatible reduction and the induction hypothesis give $\mathrm{\Lambda }u::\kappa .e$.

For type application, write $P={\mathsf{pre}}_{\mathsf{Id}}(\mathrm{\forall }u::\kappa .A)$ and $Q={\mathsf{pre}}_{\mathsf{Id}}(C)$. The decisive contractions are If the last rule of $\mathcal{D}$ is conversion from $A$ to $B$, the induction hypothesis unquotes the unchanged term $q$ at $A$, and constructor conversion assigns the same term type $B$. The variable, abstraction, application, constructor-abstraction, constructor-application, and conversion cases exhaust the derivation rules. ◻

Proof of Theorem 7.68 — Strong typed self-interpretation

Proof. The typing judgment follows from lemma 7.64, lemma 7.66 and the type of (7.15). By lemma 7.65, the term reduces to the prequotation with $F$ and the four cases replaced by the unquoting choices. By lemma 7.67, that term reduces to $e$. ◻

The shallow and deep representations, their internal unquoters, and the fold interface follow Brown and Palsberg [BP16]; the typing and reduction obligations used here are stated and proved locally.

Proof of Corollary 7.69 — Separation of represented beta classes

Proof. Mixed beta equivalence is a congruence, so apply the same internal term $\mathsf{unquote}[\hat{A}]$ to both quotations. The two results remain equivalent. By theorem 7.68, they reduce respectively to $e_1$ and $e_2$. ◻

There is a genuine self-application calculation, but it contains a quotation, not the forbidden raw diagonal application. Let $$T_u:=\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{Op}\mathsf{Id}\alpha$$ be the type of $\mathsf{unquote}$, and let ${\mathcal{D}}_u$ be its closed typing derivation. Applying the theorem to that derivation gives $$\mathsf{unquote}[\widehat{T_u}]\widehat{{\mathcal{D}}_u}{⟹}_{\beta }^{\ast }\mathsf{unquote}.$$ Quotation remains a meta-level operation. Equation (7.16) therefore constructs no internal term of type $A\to \mathsf{Exp}\hat{A}$ and does not contradict the normalization barrier of proposition 7.57. Every term in this calculation is an ordinary well-typed term of pure $F_{\omega }$; adding no term former or reduction rule means that the strong normalization and syntactic-consistency results for that calculus remain unchanged.

Recognizing the outer constructor

Use the Church booleans The four cases need not inspect their recursive arguments: Every constructor binder without an explicit kind in (7.17) has kind $\mathsf{Ty}$. The four terms have the four case types at $K_{\mathsf{Bool}}$. Since $\mathsf{Op}{K}_{\mathsf{Bool}}\alpha {=}_{\beta }\mathsf{Bool}$, define

Proof of Theorem 7.70 — Correctness of the abstraction test

Proof. The fold calculation exposes the outermost prequotation clause. In the two abstraction clauses, the corresponding case in (7.17) discards its recursive argument and returns $\mathsf{true}$. In the two application clauses it returns $\mathsf{false}$. A closed term cannot have a free variable at its root, and conversion adds no term constructor. These exhaust the possibilities. ◻

Counting term nodes

Define Church natural numbers inside pure $F_{\omega }$ by Let $\underset{―}{n}$ denote the Church numeral obtained by applying $\mathsf{succ}$ $n$ times to $\mathsf{zero}$. Then $$\mathsf{succ}\underset{―}{n}{⟶}_{\beta }^{\ast }\underset{―}{n+1},\mathsf{plus}\underset{―}{m}\underset{―}{n}{⟶}_{\beta }^{\ast }\underset{―}{m+n}.$$ The successor equation is definitional; direct beta calculation gives the addition equation.

The size of a term counts term nodes and does not count constructors in an annotation or type argument: The cases implementing these five equations are Their types are the four case types at $K_{\mathsf{Nat}}$. Therefore

Proof of Theorem 7.71 — Correctness of size

Proof. The induction must be slightly stronger than the closed statement, because a term abstraction exposes a variable in its body. Let $\mathcal{D}{⇝}_{F}q$ be an open prequotation. For every kind-respecting closing constructor substitution $\theta$ for the open constructor context, first apply $\theta$ to $q$. After substituting $K_{\mathsf{Nat}}$ and the four size cases, also substitute $\mathsf{one}$ for every free term variable. We prove that the result reduces to $\underset{―}{|e|}$. Constructor substitution changes annotations and type arguments but not the term-constructor count.

For a variable, the extra substitution gives $\mathsf{one}=\underset{―}{1}=\underset{―}{|x|}$. For term abstraction, the case term calculates $$\mathsf{sizeAbs}[\cdots ](\lambda x:\mathsf{Nat}.q^{\prime }){⟶}_{\beta }^{\ast }\mathsf{succ}(q^{\prime }[\mathsf{one}/x]).$$ The induction hypothesis gives $q^{\prime }[\mathsf{one}/x]{⟶}_{\beta }^{\ast }\underset{―}{|e|}$, so (7.18) gives $\underset{―}{1+|e|}$. Term application gives $$\mathsf{succ}(\mathsf{plus}\underset{―}{|e_1|}\underset{―}{|e_2|}){⟶}_{\beta }^{\ast }\underset{―}{1+|e_1|+|e_2|}.$$

In type abstraction, the recursive value is $\mathrm{\Lambda }u::\kappa .q^{\prime }$. Calculation (7.10), with $X=\mathsf{Nat}$, reduces the stripping expression to $$q^{\prime }[S_{\kappa }/u].$$ Apply the body induction hypothesis to the closing substitution $\theta [u\mapsto S_{\kappa }]$. It is kind respecting because $⊢S_{\kappa }::\kappa$, and it gives the required size of $q^{\prime }[S_{\kappa }/u]$. Thus term size ignores the substituted type and remains $|e|$. The outer successor therefore gives $\underset{―}{1+|e|}$. In type application, $\mathsf{sizeTApp}$ ignores the instantiation function and returns the successor of the operator size, namely $\underset{―}{1+|e|}$. Conversion changes neither prequotation nor size. This proves the strengthened assertion in every case. With an empty term context, the fold calculation yields the theorem. ◻

Testing beta-normality

A Boolean does not carry enough information through an application. To decide whether $e_1{e}_2$ is normal, one must know not only that $e_1$ is normal, but also that it is neutral and therefore cannot become a lambda redex at the root. We carry two booleans.

Define Define the three pairs $$\mathsf{TT}:=\mathsf{bools}\mathsf{true}\mathsf{true},\mathsf{TF}:=\mathsf{bools}\mathsf{true}\mathsf{false},\mathsf{FF}:=\mathsf{bools}\mathsf{false}\mathsf{false}.$$

Proof of Lemma 17.19 — Normal applications have neutral operators

Proof. For completeness, if a normal operator is not neutral, the grammar says it is a term abstraction or a type abstraction. Typing rules out the wrong one: a type abstraction has universal type, not arrow type, and a term abstraction has arrow type, not universal type. A final conversion cannot identify these heads, because constructor normalization gives distinct normal-form heads for $\to$ and $\mathrm{\forall }$. Hence an arrow-typed nonneutral normal operator is a term abstraction, producing a term beta-redex, and a universal-typed one is a type abstraction, producing a type-application redex. This proves both directions of (7.20). ◻

Now define the four cases: They inhabit the four case types at $K_{\mathsf{Bools}}$. The public test returns the first component: with type $\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{Bool}$.

Proof of Lemma 7.73 — The three-state invariant

Proof. Induct on the source typing derivation. A variable is replaced by $\mathsf{TT}$, as required.

For a term abstraction, $\mathsf{nfAbs}$ applies the recursive function to $\mathsf{TT}$, exactly the value assigned to the newly bound variable. By the induction hypothesis the first projection is true precisely when the body is normal. The second result component is false. The result is therefore $\mathsf{TF}$ for a normal abstraction and $\mathsf{FF}$ for a nonnormal one.

For term application, let $p$ and $q$ be the two recursive result pairs. The case puts the same Boolean $$(\mathsf{snd}p)\mathsf{and}(\mathsf{fst}q)$$ in both components. By the induction hypotheses this Boolean is true exactly when the operator is normal and neutral and the operand is normal. By (7.20), this is exactly when the whole application is normal; in that event the application is neutral. Thus the result is $\mathsf{TT}$ in the normal case and $\mathsf{FF}$ otherwise.

For type abstraction, the stripping calculation (7.10) with $X=\mathsf{Bools}$ selects the body at $S_{\kappa }$. Apply the body induction hypothesis to the closing substitution $\theta [u\mapsto S_{\kappa }]$, which is kind respecting because $⊢S_{\kappa }::\kappa$. The case copies its first component and sets the second to false, giving $\mathsf{TF}$ exactly when the body, and hence the abstraction, is normal; otherwise it gives $\mathsf{FF}$.

For type application, the case copies the operator’s second component into both result positions. It therefore returns $\mathsf{TT}$ exactly when the operator is normal and neutral, and $\mathsf{FF}$ otherwise. This is exactly the second equivalence of (7.20); a normal type application is itself neutral. Conversion changes no term and hence no state. The application equation in (7.20) holds exactly when the operator is neutral-normal and the operand is normal. ◻

Proof of Theorem 7.74 — Correctness of the normal-form test

Proof. By the fold calculation and lemma 7.73, the intermediate pair is $\mathsf{TT}$ or $\mathsf{TF}$ precisely when $e$ is normal, and is $\mathsf{FF}$ otherwise. Its first projection is respectively $\mathsf{true}$ or $\mathsf{false}$. ◻

Typed CPS consumers

Continuation-passing style (CPS) replaces a computation returning $A$ by a computation that receives a continuation $A\to B$ and sends its result to that continuation. The common answer operator and result family for the call-by-name and call-by-value folds are $$\mathsf{Ct}:=\lambda A::\mathsf{Ty}.\mathrm{\forall }B::\mathsf{Ty}.(A\to B)\to B,\mathsf{CPS}:=\mathsf{Op}\mathsf{Ct}.$$ The call-by-name case operators are the following pure $F_{\omega }$ terms: They have the four case types at $\mathsf{Ct}$, so their fold has type $${\mathsf{cps}}_{\mathrm{n}}:\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{CPS}\alpha .$$ The call-by-name abstraction case performs the continuation transfer. For $f:\mathsf{Ct}A\to \mathsf{Ct}B$ and $k:(\mathsf{Ct}A\to \mathsf{Ct}B)\to V$, $${\mathsf{cpsAbs}}_{\mathrm{n}}[A][B]f[V]k\stackrel{typebetaandtermbeta}{{⟶}_{\beta }^{\ast }}kf.$$ The application $kf$ has type $V$, the codomain of the continuation. Thus this calculation proves the declared case typing; it does not assert an operational simulation of source evaluation. The call-by-value artifact uses the same three application and type cases. It replaces the abstraction case by and its fold has the same public type $\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{CPS}\alpha$.

Construction boundaries

For every derivation $\mathcal{D}$ of $e:A$, the external map constructs $\hat{\mathcal{D}}:\mathsf{Exp}\hat{A}$. The internal term $$\mathsf{unquote}:\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{Op}\mathsf{Id}\alpha$$ sends this representation back to a term of $A$. Each CPS fold instead has type $\mathrm{\forall }\alpha ::U.\mathsf{Exp}\alpha \to \mathsf{CPS}\alpha$ for its fixed continuation operator. The first map is derivation-directed; the latter two are $F_{\omega }$ terms. These types neither make every inhabitant of $\mathsf{Exp}\hat{A}$ a quotation nor assert that the CPS term simulates source evaluation.

The classical diagonal obstruction also still applies internally at the numeric interface. There is no closed $V:\mathsf{Nat}\to \mathsf{Nat}\to \mathsf{Nat}$ such that every closed $f:\mathsf{Nat}\to \mathsf{Nat}$ has a numeral $\underset{―}{a}$ with $V\underset{―}{a}\underset{―}{n}{=}_{\beta }f\underset{―}{n}$ for every $n$. Otherwise $d:=\lambda n.\mathsf{succ}(Vnn)$ would have an index $\underset{―}{a}$, and the instance at $\underset{―}{a}$ would equate a Church numeral with its successor. Strong normalization and confluence distinguish those normal forms. Typed self-representation evades the raw diagonal only through its type index; it does not enumerate all total numeric functions.