Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study

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

The untyped generator $\mathsf{pow}(1,x)=x$ and $\mathsf{pow}(n+1,x)=x\cdot \mathsf{pow}(n,x)$ should turn a known exponent three into future code $x\cdot (x\cdot x)$. If quotation captures a generation-time variable, however, the alleged program may contain a free name after the generator returns. Staging needs a typing judgment that records which assumptions survive quotation.

The modal box closes future code

Fix simple types $A,B::=b\mid A\to B\mid ◻A$ and terms $$M,N::=x\mid \lambda x:A.M\mid MN\mid \mathsf{box}M\mid \mathsf{let}\mathsf{box}u=M\mathsf{in}N.$$ The judgment $\mathrm{\Delta };\mathrm{\Gamma }⊢M:A$ separates modal assumptions $u::A\in \mathrm{\Delta }$, available under boxes, from ordinary assumptions $x:A\in \mathrm{\Gamma }$, available only at the present stage.

$x:A\in \mathrm{\Gamma }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:A$

$u::A\in \mathrm{\Delta }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢u:A$

$\mathrm{\Delta };\mathrm{\Gamma },x:A⊢M:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x:A.M:A\to B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢M:A\to B$$\mathrm{\Delta };\mathrm{\Gamma }⊢N:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢MN:B$

$\mathrm{\Delta };\varnothing ⊢M:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{box}M:◻A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢M:◻A$$\mathrm{\Delta },u::A;\mathrm{\Gamma }⊢N:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{let}\mathsf{box}u=M\mathsf{in}N:B$

This is the pure dual-context modal-S4 calculus $\mathsf{Tstage}$. Rule T-Box empties the ordinary context. It accepts $u::b;\varnothing ⊢\mathsf{box}u:◻b$, but rejects $\varnothing ;x:b⊢\mathsf{box}x:◻b$. The rejection is the scope-extrusion counterexample, not a missing coercion.

Code values are $\mathsf{box}M$. Staged reduction has two contractions and five congruence families:

$(\lambda x:A.M)N⟶M[N/x]$

$\mathsf{let}\mathsf{box}u=\mathsf{box}M\mathsf{in}N⟶N[M/u]$

$M⟶M^{\prime }$

$\lambda x:A.M⟶\lambda x:A.M^{\prime }$

$M⟶M^{\prime }$

$MN⟶M^{\prime }N$

$N⟶N^{\prime }$

$MN⟶M{N}^{\prime }$

$M⟶M^{\prime }$

$\mathsf{let}\mathsf{box}u=M\mathsf{in}N⟶\mathsf{let}\mathsf{box}u=M^{\prime }\mathsf{in}N$

$N⟶N^{\prime }$

$\mathsf{let}\mathsf{box}u=M\mathsf{in}N⟶\mathsf{let}\mathsf{box}u=M\mathsf{in}{N}^{\prime }$

There is no congruence beneath $\mathsf{box}$: its body is future syntax.

The modal eta expansion is $M:◻A\mapsto \mathsf{let}\mathsf{box}u=M\mathsf{in}\mathsf{box}u$, with $u$ fresh. Its typing derivation first applies T-LetBox; in the body, T-MVar derives $u:A$ and T-Box closes the empty ordinary context. Thus eta expresses local completeness of elimination followed by introduction. It is an expansion principle, not a staged evaluation step.

If multiplication is a modal constant $m::b\to b\to b$, repeated T-LetBox constructs $$u::b;\varnothing ⊢\mathsf{box}(mu(muu)):◻b.$$ Each occurrence of $u$ is modal. Replacing it by an ordinary $x:b$ invalidates the premise of T-Box.

Proof of Lemma 129.1 — Dual substitution

Proof. For ordinary substitution, induct on the derivation of $M$. The variable case uses the second premise when its variable is $x$. Under T-Box, the premise has empty ordinary context, so $x$ cannot occur; weakening the unchanged premise concludes the case. Abstraction and application use their induction hypotheses. In T-LetBox, apply them to both premises after alpha-renaming the modal binder away from $N$.

For modal substitution, use the same induction. Rule T-MVar uses the closed ordinary-context premise when its variable is $u$. Rule T-Box admits that premise because modal assumptions remain available under a box. The binder case is handled by alpha-renaming. These are all six rule families. ◻

Call a subterm occurrence persistent when it lies beneath a box; other occurrences are eliminable. A term is irreducible when none of the seven staged rules applies. In the labelled syntax, labels are inert metadata: a contraction transports labels on retained syntax and on every copied substitution instance, and no operational rule creates or erases a label.

Proof of Theorem 129.2 — Local eliminability and inert-label persistence

Proof. Induction on the finite reduction sequence, using the two substitution clauses at the two contractions, gives $\varnothing ;\varnothing ⊢M^{\prime }:◻A$. A simultaneous induction on a closed irreducible typing derivation gives the needed canonical-form fact. The variable case is impossible. An abstraction has arrow type. In an application, the induction hypothesis makes a closed irreducible function of arrow type an abstraction, so beta would apply. In a let-box term, the induction hypothesis makes its irreducible scrutinee a box, so let-box beta would apply. Therefore a closed irreducible term of type $◻A$ is $\mathsf{box}N$. Every occurrence belonging to its body $N$ lies below that box.

For persistence, induct on the staged reduction. In ordinary beta, the modal typing restriction prevents the substituted ordinary variable from occurring beneath a box; this follows by induction on the body typing derivation. In let-box beta, every occurrence of the substituted code body was labelled in the boxed premise. Congruence preserves labels by the induction hypothesis. There is no box congruence, so no reduction changes a labelled occurrence already beneath a box. These are the two contractions and five congruence families; labels add no reduction rule. This is a theorem of the displayed unlabelled dual-context calculus extended with inert occurrence metadata. Davies and Pfenning’s source calculus also has labelled expressions $E^{\ell }$, an explicit unlabelling contraction, and labelled case analysis. Its Theorems 5–6 prove eliminability and persistence for that richer operational system [DP01]; the local theorem neither imports nor silently omits those additional rules. ◻

Proof of Theorem 129.3 — Subject reduction and scope safety

Proof. Induct on the reduction derivation. Beta uses ordinary substitution. Let-box beta uses modal substitution. Compatible cases rebuild their typing rule with the induction hypothesis. If a closed term evaluates to a code value, preservation gives $\varnothing ;\varnothing ⊢\mathsf{box}N:◻A$; inversion of T-Box gives the conclusion. ◻

Related staging judgments do not share rules

MetaML-style quotation and escape use stage-indexed contexts and may include cross-stage persistence. A sound CSP rule must restrict the persisted values; persisting a mutable reference would let future code retain a cell from a completed run. $\mathsf{Tstage}$ has no CSP rule, reference, or run operator, so theorem 129.3 says nothing about that extension. For comparison only, fix the pure two-stage MetaML fragment with $\tau ::=b\mid \tau \to \tau \mid {\mathsf{Code}}_{\alpha }\tau$, stage words $A$, and judgments $\mathrm{\Gamma }{⊢}_{A}M:\tau$. Its deliberately restrictive persistent-value predicate is generated by

$c_b\text{ is a closed immutable literal}$

$\mathsf{Pers}(c_b:b)$

$\varnothing {⊢}_A⟨M{⟩}_{\beta }:{\mathsf{Code}}_{\beta }\tau$$\mathrm{Loc}(M)=\varnothing$

$\mathsf{Pers}(⟨M{⟩}_{\beta }:{\mathsf{Code}}_{\beta }\tau )$

Here $\mathrm{Loc}(M)$ is the finite set of store locations occurring in $M$; it is empty throughout the pure fragment. There is no persistent function clause. The three-rule delta is

$\mathrm{\Gamma }{⊢}_{A\alpha }M:\tau$

$\mathrm{\Gamma }{⊢}_A⟨M{⟩}_{\alpha }:{\mathsf{Code}}_{\alpha }\tau$

$\mathrm{\Gamma }{⊢}_{A}M:{\mathsf{Code}}_{\alpha }\tau$

$\mathrm{\Gamma }{⊢}_{A\alpha }{\sim }_{\alpha }M:\tau$

$\mathrm{\Gamma }{⊢}_{A}v:\tau \mathsf{Pers}(v:\tau )$

$\mathrm{\Gamma }{⊢}_{A\alpha }{\mathrm{\%}}_{\alpha }v:\tau$

The side condition is load-bearing. If it admitted locations, then $$\mathsf{let}r=\mathsf{ref}0\mathsf{in}⟨\mathsf{get}({\mathrm{\%}}_{\alpha }r){⟩}_{\alpha }$$ would return code containing $r$ after the allocating run ended. The two constructors of $\mathsf{Pers}$ reject that location. This card states no store theorem; it exposes one exact safe fragment and the smallest premise that a reference-bearing extension would have to replace with a world-indexed store invariant.

The source comparison is not a renaming of $\mathsf{Tstage}$. Davies and Pfenning’s two-level Mini-ML has run-time types $\tau ::=\mathsf{nat}\mid \tau \to \tau \mid \tau \times \tau \mid 1$ and compile-time types $\sigma ::=\mathsf{nat}\mid \sigma \to \sigma \mid \sigma \times \sigma \mid 1\mid \underset{―}{\tau }$. Terms have separately underlined run-time and overlined compile-time constructors for variables, abstraction, application, fixed points, pairs, projections, unit, zero, successor, and natural-number case. The two judgments are $\mathrm{\Delta };\mathrm{\Gamma }{⊢}^{r}e:\tau$ and $\mathrm{\Delta }{⊢}^{c}e:\sigma$. For $p\in \{r,c\}$, every constructor has the following phase-indexed schema (with ${\mathcal{C}}_r=\mathrm{\Delta };\mathrm{\Gamma }$, ${\mathcal{C}}_c=\mathrm{\Delta }$, and a binder added to the corresponding context):

$x:T\in {\mathcal{C}}_p$

${\mathcal{C}}_p{⊢}^{p}x:T$

${\mathcal{C}}_p,x:T_1{⊢}^{p}e:T_2$

${\mathcal{C}}_p{⊢}^p{\lambda }^{p}x:T_1.e:T_1\to T_2$

${\mathcal{C}}_p{⊢}^p{e}_1:T_1\to T_2$${\mathcal{C}}_p{⊢}^p{e}_2:T_1$

${\mathcal{C}}_p{⊢}^p{e}_1{@}^p{e}_2:T_2$

${\mathcal{C}}_p,x:T{⊢}^{p}e:T$

${\mathcal{C}}_p{⊢}^p{\mathsf{fix}}^{p}x:T.e:T$

${\mathcal{C}}_p{⊢}^p{e}_1:T_1$${\mathcal{C}}_p{⊢}^p{e}_2:T_2$

${\mathcal{C}}_p{⊢}^p⟨e_1,e_2{⟩}^p:T_1\times T_2$

${\mathcal{C}}_p{⊢}^{p}e:T_1\times T_2$

${\mathcal{C}}_p{⊢}^p{\mathsf{proj}}_i^p(e):T_i$

${\mathcal{C}}_p{⊢}^p⟨{⟩}^p:1$

${\mathcal{C}}_p{⊢}^p{\mathsf{z}}^p:\mathsf{nat}$

${\mathcal{C}}_p{⊢}^{p}e:\mathsf{nat}$

${\mathcal{C}}_p{⊢}^p{\mathsf{s}}^{p}e:\mathsf{nat}$

${\mathcal{C}}_p{⊢}^p{e}_0:\mathsf{nat}$${\mathcal{C}}_p{⊢}^p{e}_z:T$${\mathcal{C}}_p,x:\mathsf{nat}{⊢}^p{e}_s:T$

${\mathcal{C}}_p{⊢}^p{\mathsf{case}}^p{e}_0\mathsf{of}\mathsf{z}\Rightarrow e_z\mid \mathsf{s}x\Rightarrow e_s:T$

The two phase-transition rules are the entire rule delta:

$\mathrm{\Delta }{⊢}^{c}e:\underset{―}{\tau }$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}^{r}e:\tau$

$\mathrm{\Delta };\varnothing {⊢}^{r}e:\tau$

$\mathrm{\Delta }{⊢}^{c}e:\underset{―}{\tau }$

The mutually recursive translation $\Vert -\Vert$ on run-time syntax and $|-|$ on compile-time syntax is homomorphic on each phase’s constructors, maps $|\underset{―}{\tau }|$ to $◻\Vert \tau \Vert$, and has the decisive equations $$\Vert \bar{e}\Vert ={\mathsf{unbox}}_1|\bar{e}|,|\underset{―}{e}|=\mathsf{box}\Vert \underset{―}{e}\Vert .$$ Here the target is the source’s implicit multi-world Mini-ML, whose ${\mathsf{unbox}}_1$ discharges one context-stack boundary. Write $\mathcal{S}{⊢}^{i}M:A$ for that target judgment: $\mathcal{S}$ is the stack of ordinary contexts, variables are selected from its active component, $\mathsf{box}$ pushes an empty component, and ${\mathsf{unbox}}_1$ pops one component. Write $\mathcal{S},x:T$ for extension of its active component. The function and modal rules are

$x:T\in \mathrm{last}(\mathcal{S})$

$\mathcal{S}{⊢}^{i}x:T$

$\mathcal{S},x:T{⊢}^{i}M:U$

$\mathcal{S}{⊢}^i\lambda x:T.M:T\to U$

$\mathcal{S}{⊢}^{i}M:T\to U$$\mathcal{S}{⊢}^{i}N:T$

$\mathcal{S}{⊢}^{i}MN:U$

For every ordinary context $\mathrm{\Gamma }$, the two boundary rules are

$\mathcal{S};\varnothing {⊢}^{i}M:T$

$\mathcal{S}{⊢}^i\mathsf{box}M:◻T$

$\mathcal{S}{⊢}^{i}M:◻T$

$\mathcal{S};\mathrm{\Gamma }{⊢}^i{\mathsf{unbox}}_{1}M:T$

Thus I-Box enters one future world and I-Unbox1 uses code from its immediate predecessor; the latter is not an unindexed run operation. The remaining constructor schemas are

$\mathcal{S},x:T{⊢}^{i}M:T$

$\mathcal{S}{⊢}^i\mathsf{fix}x:T.M:T$

$\mathcal{S}{⊢}^{i}M:T_1$$\mathcal{S}{⊢}^{i}N:T_2$

$\mathcal{S}{⊢}^i⟨M,N⟩:T_1\times T_2$

$\mathcal{S}{⊢}^{i}M:T_1\times T_2$

$\mathcal{S}{⊢}^i{\mathsf{proj}}_j(M):T_j$

$\mathcal{S}{⊢}^i⟨⟩:1$

$\mathcal{S}{⊢}^i\mathsf{z}:\mathsf{nat}$

$\mathcal{S}{⊢}^{i}M:\mathsf{nat}$

$\mathcal{S}{⊢}^i\mathsf{s}M:\mathsf{nat}$

$\mathcal{S}{⊢}^{i}M:\mathsf{nat}$$\mathcal{S}{⊢}^i{M}_z:T$$\mathcal{S},x:\mathsf{nat}{⊢}^i{M}_s:T$

$\mathcal{S}{⊢}^i\mathsf{case}M\mathsf{of}\mathsf{z}\Rightarrow M_z\mid \mathsf{s}x\Rightarrow M_s:T$

These displayed schemas are every target family used by the translation. This is the exact JACM card on printed pages 35–40; the term translation is on printed page 39 and the embedding theorem is on printed page 40. It is not the dual-context calculus above.

Proof of Theorem 129.4 — Two-level embedding

Proof. This is an exact import of Davies–Pfenning Theorem 15 [DP01]. The forward and reflection directions are proved simultaneously by structural induction on the two translations. Every homomorphic constructor uses the corresponding source and target rule plus its induction hypotheses. The only nonhomomorphic cases are 2-Down and 2-Up: the former translates to ${\mathsf{unbox}}_1$, and target inversion recovers the compile-time premise; the latter translates to $\mathsf{box}$, and target inversion recovers the empty run-time context. Those inversions also prove that a target type in the translation image reflects to the unique source phase type. These cases and the homomorphic schema cover every printed rule family. ◻

For a self-contained arithmetic comparison, fix annotated terms $$a::=n^S\mid x_s^S\mid x_d^D\mid a_1{+}^b{a}_2\mid a_1{\cdot }^b{a}_2,b\in \{S,D\}.$$ An $S$-operation requires two $S$-operands. A $D$-operation accepts either binding time and embeds a computed numeral as a residual numeral. The formation judgment $s{⊢}_{A}a:b$, where $s$ is defined on every static variable, has rules

$s{⊢}_A{n}^S:S$

$x_s\in \mathrm{dom}(s)$

$s{⊢}_A{x}_s^S:S$

$s{⊢}_A{x}_d^D:D$

$s{⊢}_A{a}_1:S$$s{⊢}_A{a}_2:S$

$s{⊢}_A{a}_1{\odot }^S{a}_2:S$

$s{⊢}_A{a}_1:b_1$$s{⊢}_A{a}_2:b_2$

$s{⊢}_A{a}_1{\odot }^D{a}_2:D$

Define ${\mathsf{specialize}}_A$ by recursion on a derivation of that judgment: where $\odot \in \{+,\cdot \}$, ${\mathsf{specialize}}_A(a_i,s)=\mathsf{val}(n_i)$ in the static equation, ${\mathsf{specialize}}_A(a_i,s)=q_i$ in the dynamic equation, $\lfloor \mathsf{val}(n)\rfloor =n$, and $\lfloor \mathsf{code}(r)\rfloor =r$. Its annotation erasure $|a{|}_A$ removes superscripts. This grammar is the nonrecursive, conditional-free arithmetic sublanguage of the Scheme0 source card definition 127.1: $x_s^S$ marks a variable in the static environment, $x_d^D$ marks a residual variable, and the superscript on an operator is its binding-time annotation. No Scheme0 call, conditional, memo-table operation, or annotation inference is translated here.

For a residual arithmetic term $r$, define its Tstage body $⌜r{⌝}_A$ by mapping a numeral $n$ to a modal numeral constant $\overline{n}::b$, a residual variable $x_d$ to the modal variable $x_d::b$, and $r_1\odot r_2$ to $\overline{\odot }⌜r_1{⌝}_A⌜r_2{⌝}_A$, where $\overline{\odot }::b\to b\to b$ is modal. For a specialization result $q$, let ${\mathrm{\Delta }}_d(a,q)$ contain $\overline{n}::b$ for every numeral $n$ occurring in $\lfloor q\rfloor$, $\overline{\odot }::b\to b\to b$ for every operator occurring in $\lfloor q\rfloor$, and $x_d::b$ for every dynamic variable of $a$. This context is finite because $a$ and $q$ are finite syntax. Put $${\mathsf{code}}_A(r):=\mathsf{box}⌜r{⌝}_A$$ and use the meta-level observation $${\mathsf{exec}}_A({\mathsf{code}}_A(r),d)=n⟺{\mathsf{eval}}_A(r,d)=n.$$ Neither ${\mathsf{exec}}_A$ nor ${\mathsf{eval}}_A$ is a reduction rule of $\mathsf{Tstage}$.

Proof of Proposition 129.5 — Type preservation for the Scheme0 arithmetic bridge

Proof. Induct on the derivation of $s{⊢}_{A}a:b_A$, retaining the equation that defines $q$. A numeral specializes to $\mathsf{val}(n)$, and a static variable specializes to $\mathsf{val}(s(x_s))$; T-MVar types the corresponding modal numeral constant at $b$. A dynamic variable specializes to $\mathsf{code}(x_d)$, and T-MVar types $x_d:b$.

In A-Op-S, both operands specialize to recorded numerals and the result is $\mathsf{val}(n_1\odot n_2)$, so the numeral-constant case applies. In A-Op-D, the two induction hypotheses type $⌜\lfloor q_1\rfloor {⌝}_A$ and $⌜\lfloor q_2\rfloor {⌝}_A$ at $b$. Rule T-MVar types $\overline{\odot }:b\to b\to b$; two uses of T-App give the translated residual operation type $b$. These are all formation rules. In every case, T-Box applies because the ordinary context is empty, yielding the second judgment. ◻

Proof of Lemma 129.6 — Arithmetic specialization for both binding times

Proof. Induct on the displayed binding-time derivation, with the assertion quantified over its conclusion $b$ and output $q$. A numeral evaluates to itself. A static variable is looked up in $s$, and a dynamic variable is looked up in $d$; these are exactly their specialized outputs. For A-Op-S, both induction hypotheses yield the recorded numerals, and specialization computes the same primitive. For A-Op-D, apply the induction hypothesis separately to each premise, whether its conclusion is $S$ or $D$. Erasure evaluates the primitive on those two values, while specialization embeds each $\mathsf{val}(n_i)$ as the residual numeral $n_i$ and leaves each $\mathsf{code}(r_i)$ as $r_i$. The residual primitive therefore receives the identical pair of values. These are all three leaves, both primitive symbols, and both operation rules. ◻

Proof of Proposition 129.7 — Annotated arithmetic commuting instance

Proof. Apply lemma 129.6 with $q=\mathsf{code}(r)$. Its right side is ${\mathsf{eval}}_A(r,d)$, which is equivalent by definition to ${\mathsf{exec}}_A({\mathsf{code}}_A(r),d)$. Symmetry gives the displayed orientation. The primitive-definedness condition is unchanged. ◻

Tagless-final staging is another interface. Begin with the initial syntax $$t::=\mathsf{lit}(n)\mid \mathsf{var}(x)\mid \mathsf{mul}(t,t).$$ For an environment $d$, its evaluator has the three equations Its serializer is the fold that maps a literal to its decimal numeral, a variable to its name, and multiplication to the parenthesized concatenation $\mathtt{\text{(}}s\mathtt{\text{*}}r\mathtt{\text{)}}$. These are two algebras for the same signature $$\mathsf{lit}:\mathbb{N}\to R,\mathsf{var}:\mathsf{Var}\to R,\mathsf{mul}:R\to R\to R.$$

The final representation of an initial tree $t$ is the polymorphic operation $\hat{t}$ that accepts such an algebra and returns its interpretation. The evaluator and serializer are therefore added one at a time by choosing $R=(\mathsf{Var}\to \mathbb{N})\to \mathbb{N}$ and $R=\mathsf{String}$, respectively. Structural induction gives their exact common representation property.

Proof of Proposition 129.8 — Pure tagless-final representation

Proof. Induct on $t$. A literal and a variable use the corresponding algebra operation on both sides. A multiplication node applies the induction hypotheses to its two children and then the same $\mathsf{mul}$ operation. These are all three constructors. ◻

Now add a partial-evaluation algebra. Its carrier is Literals are known, variables are later, and multiplication computes on two known inputs: $${\mathsf{mul}}_{\mathsf{pe}}(\mathsf{known}(n_1),\mathsf{known}(n_2))=\mathsf{known}(n_1{n}_2).$$ For every other pair $(q_1,q_2)$, it residualizes: $${\mathsf{mul}}_{\mathsf{pe}}(q_1,q_2)=\mathsf{later}(\mathsf{mul}(\mathsf{reify}(q_1),\mathsf{reify}(q_2))).$$ For $t_0=\mathsf{mul}(\mathsf{lit}(2),\mathsf{mul}(\mathsf{lit}(3),\mathsf{lit}(4)))$, evaluation returns $24$, serialization returns $\mathtt{\text{(2*(3*4))}}$, and partial evaluation returns $\mathsf{known}(24)$. For $t_1=\mathsf{mul}(\mathsf{lit}(2),\mathsf{mul}(\mathsf{var}(x),\mathsf{lit}(3)))$, partial evaluation returns the same tree under $\mathsf{later}$; the algebra performs no reassociation rule.

Proof of Proposition 129.9 — Pure tagless-final partial-evaluation equation

Proof. Induct on $t$. Literal and variable cases are their defining equations. For multiplication, apply both induction hypotheses. When both outputs are known, their recorded naturals are the two source evaluations, so multiplying them is sound. Otherwise reification rebuilds multiplication from two reified outputs, and the evaluator uses the induction hypotheses componentwise. These are the two partial-evaluator alternatives. ◻

The course examples separately calculate evaluation, serialization, and de Bruijn partial evaluation. Those examples concern the displayed tagless final algebra; they neither represent arbitrary $\mathsf{Tstage}$ terms nor prove a host optimizer correct [CKcS09].

The optimizing evaluators of Wei, Tan, and Zhong form another separate card [WTZ26]. Their binding-time-annotated object language is interpreted successively by a stateful evaluator, a one-continuation evaluator, a two-continuation evaluator, a delimited-control evaluator, and a CEKM machine. The two continuations separate the rest of the generated expression from the boundary at which pending bindings are inserted. The optimizing evaluator then composes seven independently selectable reflection clauses in this priority order: $$\mathsf{atom},\mathsf{inline},\mathsf{fold},\mathsf{partialStatic},\mathsf{simplifyCond},\mathsf{CSE},\mathsf{DCE},$$ followed by a default clause which introduces a fresh residual let-binding. The ordering is part of this implementation card: changing it can expose a different expression to a later clause.

For example, apply only the CSE clause to the dynamic expression $$(2\cdot 3)+(2\cdot 3).$$ The first multiplication is inserted as $x_0$. The cache maps the second, syntactically equal pure multiplication to the same $x_0$, and the default clause names the sum. The printed result is $$\mathsf{let}{x}_0=2\cdot 3\mathsf{in}\mathsf{let}{x}_1=x_0+x_0\mathsf{in}{x}_1.$$ The calculation establishes only the displayed result. It does not prove contextual equivalence of the evaluator families, soundness of every optimization, or compiler correctness for LMS, MetaOCaml, or $\mathsf{Tstage}$.

To connect the final interface back to the modal card, define one modal literal constant $\bar{n}::b$ for each numeral, a modal variable constant $\bar{x}::b$ for each object variable, and a modal multiplication constant $m::b\to b\to b$. Then define The two let-boxes sequence the generator’s recursive results; modal substitution yields $G(\mathsf{mul}(\mathsf{lit}(2),\mathsf{lit}(3))){⟶}^{\ast }\mathsf{box}(m\bar{2}\bar{3})$. The modal calculus treats these constants symbolically; it contains no numeral, variable-lookup, or multiplication reduction. Changing the outer sequencing order changes the evaluation order of the generators even though the final pure code is alpha-equivalent. With effectful generators, order must instead be preserved by naming the left result before evaluating the right: $$\mathsf{let}a=G(t)\mathsf{in}\mathsf{let}b=G(u)\mathsf{in}\mathsf{combine}(a,b).$$ This is a let-insertion calculation, not an equation that permits reordering.

MetaOCaml’s code types, quotation, escape, run, CSP, and let insertion form one system card. Lightweight modular staging instead represents object operations by a host interface and uses host normalization plus explicit code combinators [RO10]. These cards differ from the modal calculus in their syntax, typing judgments, and reduction relations. Neither supplies a theorem about $\mathsf{Tstage}$: such a transfer would require a typed translation and a simulation theorem.

MacoCaml is a third card. Its core types and expressions include The source elaboration judgment is $${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^{\star }e:\tau ⇝e^{\prime };{\sigma }_2,\star \in \{c,s,q\}.$$ It records the input heap ${\sigma }_1$, compile-time evaluation context $\mathrm{\Omega }$, type context $\mathrm{\Gamma }$, integer level $n$, compiler mode $\star$, elaborated core expression $e^{\prime }$, and output heap ${\sigma }_2$. A local variable declaration records the same level at which it may be used. Mode $c$ is ordinary compilation, $s$ is compile-time computation inside a top-level splice, and $q$ is quotation. The staging rules are

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_{n+1}^{q}e:\tau ⇝e^{\prime };{\sigma }_2$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^{c\vee s}⟨e⟩:\mathsf{Code}\tau ⇝⟨e^{\prime }⟩;{\sigma }_2$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_{n-1}^{s}e:\mathsf{Code}\tau ⇝e^{\prime };{\sigma }_2$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^q\mathrm{\$}e:\tau ⇝\mathrm{\$}{e}^{\prime };{\sigma }_2$

Here $c\vee s$ abbreviates one instance for each of the two modes. A top-level splice instead uses compile-time evaluation:

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_{n-1}^{s}e:\mathsf{Code}\tau ⇝e^{\prime };{\sigma }_2$${\sigma }_2;\mathrm{\Omega }⊢e^{\prime }{⟶}_0^{\ast }⟨v⟩;{\sigma }_3$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^c\mathrm{\$}e:\tau ⇝v;{\sigma }_3$

Runtime definitions $\mathsf{def}k=e$ bind $k$ at level zero; macro definitions ${\mathsf{def}}^{\downarrow }m=e$ bind $m$ at level minus one. A top-level splice is the compilation interface: typing interleaves with its evaluation, requires a quoted result, and inserts the quoted body into the compiled module. A compiled module contains no top-level splice.

Composition shifts levels explicitly. Importing a module at level zero makes its runtime definitions available at level zero; an ${\mathsf{import}}^{\downarrow }$ shifts them to level minus one for compile-time use. Macro-bearing modules compose through those leveled imports rather than through textual substitution. Quotation retains binding information. Splice elaboration chooses each binder outside the identifiers occurring in the caller module, quoted value, and generated body before binder insertion. In the paper’s power example the generated parameter is therefore $x_1$, which does not occur in the caller; the caller’s $x$ cannot be captured. The compiled code for exponent five is $$\lambda x_1.x_1\cdot (x_1\cdot (x_1\cdot (x_1\cdot (x_1\cdot 1)))),$$ and applying it to three returns $243$.

Proof of Theorem 129.10 — MacoCaml elaboration soundness

Proof. This is the exact expression instance of the source elaboration-soundness theorem [XWNY23]. Its simultaneous induction over expression and structure elaboration uses preservation for the evaluation premise of MC-CodeGen; the level-shape conclusion prevents the returned quotation body from capturing a location at the negative typing level. The source proves the corresponding module and structure instances by the same simultaneous induction. ◻

Preservation, progress, and phase distinction belong to this exact level-indexed calculus [XWNY23]. Its quotation/composition interface is neither MetaOCaml execution nor T-Box, so those proofs strengthen neither theorem 129.3 nor theorem 129.4.

The pure Tan–Wei calculus ${\lambda }_{|2|}$ is a fourth system card [TW26]. It freezes stages $s\in \{\mathbb{1},\mathbb{2}\}$ and the surface grammar Evaluation adds the administrative forms and values A pure evaluation context $E$ contains the ordinary left-to-right application, operation, fixed-point, conditional, lift, and let frames. A reification context $P$ may additionally contain $${\lambda }_{\mathsf{c}}x.[],{\mathsf{let}}_{\mathsf{c}}x=t\mathsf{in}[],\mathsf{run}[],{\mathsf{ifz}}^{\mathbb{2}}(v,[],t),{\mathsf{ifz}}^{\mathbb{2}}(v_1,v_2,[]).$$ The decisive head step, for a name $x$ fresh for $P,E,t$, is $$P[E[\mathsf{reflect}t]]⟶P[{\mathsf{let}}_{\mathsf{c}}x=t\mathsf{in}E[\mathsf{code}x]].$$ Thus a reflected fragment is named once at its reification boundary. The freshness premise and the restriction of $E$ to ordinary pure frames are what preserve binding and left-to-right evaluation order.

The static card has The judgment $\mathrm{\Gamma }{⊢}^{s}t:\tau \mid ϵ$ checks a term at a specified stage. The reification judgment $\mathrm{\Gamma }⊢t:\tau \mid ϵ$ either embeds a pure stage-one term or packages a fragment as complete code:

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }⊢t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}t:\mathsf{frag}(\tau )\mid ϵ$

$\mathrm{\Gamma }⊢t:\mathsf{rep}(\tau )\mid ϵ$

The rules for $\mathsf{code}$, $\mathsf{reflect}$, and inserted bindings expose the control effect:

$\mathrm{\Gamma }{⊢}^{\mathbb{2}}t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}\mathsf{code}t:\mathsf{rep}(\tau )\mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{2}}t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}\mathsf{reflect}t:\mathsf{frag}(\tau )\mid \mathrm{\top }$

$\mathrm{\Gamma }{⊢}^{\mathbb{2}}{t}_1:{\tau }_1\mid \mathrm{\perp }$$\mathrm{\Gamma },x^{\mathbb{2}}:{\tau }_1⊢t_2:\mathsf{rep}({\tau }_2)\mid ϵ$${\mathsf{WF}}^{\mathbb{2}}({\tau }_1)$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}{\mathsf{let}}_{\mathsf{c}}x=t_1\mathsf{in}{t}_2:\mathsf{rep}({\tau }_2)\mid \mathrm{\perp }$

In particular, complete code may contain divergence or a generated-stage effect and therefore is not treated as an unrestricted pure fragment. The remaining surface rules propagate the join of premise effects; every stage-two code-producing operator concludes with effect $\mathrm{\top }$. Function types at stage two require latent effect $\mathrm{\perp }$.

Stage erasure $|t|$ changes every stage annotation to $\mathbb{1}$, deletes lift, run, code, reflect, and ${\lambda }_{\mathsf{c}}$, maps inserted ${\mathsf{let}}_{\mathsf{c}}$ to ordinary let, and erases $\mathsf{rep}$, $\mathsf{frag}$, and latent effects. For stage-erased types, define the step-indexed value and term interpretations by exactly when, for every $j\le k$ and $(j,v_1,v_2)\in \mathcal{V}[[{\tau }_1]]$, $$(j,{\mathsf{app}}^{\mathbb{1}}(\lambda x.t_1,v_1),{\mathsf{app}}^{\mathbb{1}}(\lambda x.t_2,v_2))\in \mathcal{E}[[{\tau }_2]].$$ Moreover, $(k,t_1,t_2)\in \mathcal{E}[[\tau ]]$ exactly when The environment interpretation starts with $\mathcal{G}[[\varnothing ]]=\{(k,\varnothing ,\varnothing )\mid k\in \mathbb{N}\}$ and extends two substitutions with values related by $\mathcal{V}$ at every declaration $x^{\mathbb{2}}:\tau$. Write $t_1{\approx }_{\mathsf{log}}{t}_2:\tau$ when the two terms have erased typing $\mathrm{\Gamma }{⊢}^{\mathbb{2}}{t}_i:\tau \mid \mathrm{\perp }$ and all related substitution instances belong to $\mathcal{E}$ in both directions.

Contextual equivalence has a narrower observation than equality of printed base results. For every well-typed closing context $C$, $t_1{\approx }_{\mathsf{ctx}}{t}_2:\tau$ means $C[t_1]$ terminates if and only if $C[t_2]$ terminates. Distinct observable base values can be separated by a context, but the definition itself is termination-based.

Proof of Lemma 129.11 — Tan–Wei logical-relation interface

Proof. These are exact source imports: Theorems 5.4, 5.5, 5.8, and 5.3, respectively . The definitions above print their complete signatures. Within Instar/TwoLevelRec/, the Lean declarations are:

LogicalEquiv/Fundamental.lean
contains log_equiv.fundamental.

LogicalEquiv/Soundness.lean
contains log_equiv.soundness.

SemanticsPreservation/Preservation.lean
contains semantics_preservation.

CtxEquiv/Transitivity.lean
contains ctx_equiv.trans.

The imported proofs cover the compatibility families, substitution, and the reification-context case; no theorem for $\mathsf{Tstage}$, MetaOCaml, or LMS is a consequence. ◻

The extension ${\lambda }_{|2|}^{\mathsf{ref}}$ adds locations, stores of natural numbers, $\mathsf{ref}(\mathsf{nat})$, and stage-indexed allocation, get, and put. The executing ${\mathsf{alloc}}^{\mathbb{1}}$, ${\mathsf{get}}^{\mathbb{1}}$, and ${\mathsf{put}}^{\mathbb{1}}$ forms may be typed only beneath the stage-$\mathbb{2}$ judgment; the stage-two forms build fragments beneath the stage-$\mathbb{1}$ judgment. Moreover, $\mathsf{run}$ requires a store-free argument. Its world $W\subseteq \mathbb{N}\times \mathbb{N}$ is a partial bijection between locations; stores ${\sigma }_1,{\sigma }_2$ are related at $W$ when they contain equal naturals at every related pair. The value clause for references is $$(k,W,{\ell }_1,{\ell }_2)\in \mathcal{V}[[\mathsf{ref}(\mathsf{nat})]]⟺({\ell }_1,{\ell }_2)\in W.$$ The term clause quantifies over every pair of stores related by $W$: a left run terminating in steps must be matched on the right by a run to related values and stores at an extension $W^{\prime }\supseteq W$, with remaining index $k-j$. This is the exact Kripke extension of the displayed pure relation, rather than a persistence theorem for host-language references.

A forbidden first-stage reference shows why the restriction is necessary. Allocate $r=0$, lift a function whose body increments $r$, and finally lift the contents of $r$. Lifting the function executes its body during generation, so the generated answer is one; erasure leaves that body beneath a lambda and returns zero. A second counterexample makes evaluation order visible. With a first-stage $r=0$, residualize a conditional whose first branch increments and reads $r$, and whose second branch only reads $r$. Reifying the first branch first produces $\mathsf{ifz}(b,1,1)$; reifying the second first produces $\mathsf{ifz}(b,1,0)$. The erased program selects one branch before its effect, so it has the latter behavior. The accepted repair allocates $r$ with ${\mathsf{alloc}}^{\mathbb{2}}$ and uses only stage-two get and put. The first-stage store then remains empty, and generation returns $$\mathsf{let}r={\mathsf{alloc}}^{\mathbb{1}}0\mathsf{in}{\mathsf{ifz}}^{\mathbb{1}}(b,\mathsf{let}\mathrm{\_}={\mathsf{put}}^{\mathbb{1}}(r,{\mathsf{get}}^{\mathbb{1}}r+1)\mathsf{in}{\mathsf{get}}^{\mathbb{1}}r,{\mathsf{get}}^{\mathbb{1}}r).$$ Its effects occur only when the generated conditional executes, in the same order as the stage erasure.

Proof of Theorem 129.12 — Source-bounded staging-erasure equivalence

Proof. For the pure card, induct on the multistep reduction. Reflexivity gives contextual reflexivity. At a successor step, item 3 of lemma 129.11 gives equivalence of the two erasures; compose it with the induction hypothesis by item 4. At the terminal code value, $|\mathsf{code}{t}_2|=t_2$. This is the proof assembly of source Theorems 5.9–5.10 [TW26].

For the reference card, use the world-indexed versions of the fundamental, soundness, one-step, and transitivity results. The initial world and both first-stage stores are empty; the store-free run premise ensures that first-stage reduction never allocates a location. Iteration therefore yields the displayed contextual equivalence. This is source Theorem 6.4 [TW26]. Its world-indexed signature is different from the pure theorem’s signature, so neither result transfers to another staging card without a separate interpretation theorem. ◻

An evidence-bounded tower

A tower with object program $p$, interpreter $I$, and meta-interpreter $J$ evaluates $J⌜I⌝⌜p⌝$. Ordinary execution retains two dispatch layers. The comparison card is Amin–Rompf’s untyped multi-level kernel ${\lambda }^{\uparrow \downarrow }$, not $\mathsf{Tstage}$. Its source and internal syntax is Here ${\oplus }_1$ ranges over the three predicates and pair projections, and ${\oplus }_2$ over addition, subtraction, multiplication, and equality. $\mathsf{Reflect}$ and ${\mathsf{Let}}_{\mathsf{c}}$ implement ordered let insertion; they are not user quotation forms. The level parameter is the first argument of $\mathsf{Run}(b,e)$. Evaluation of $b$ to code emits a residual run; any non-code value executes the reified code at the present level: In both equations, $q={\mathsf{reify}}_{\mathsf{c}}({\mathsf{eval}}_{ms}(\rho ,e))$. The polymorphic $\mathsf{Lift}$ maps a numeral to numeral syntax, a pair componentwise, code to residual $\mathsf{Lift}$, and a closure to code by two-level eta expansion. Thus stage polymorphism is operational: the Pink interpreter abstracts over $\mathsf{maybeLift}$, instantiated by the identity for $\mathsf{eval}$ and by $\mathsf{Lift}$ for $\mathsf{evalc}$. The calculus has no typing judgment that could be imported into $\mathsf{Tstage}$.

For a Pink program $p$, write $p_{src}$ for its quoted S-expression and $[[p]]$ for its translation to administrative normal form in ${\lambda }^{\uparrow \downarrow }$. Define $${\mathsf{eval}}_1=\mathsf{eval},{\mathsf{eval}}_{n+1}={\mathsf{eval}}_n{\mathsf{eval}}_{src}.$$ The paper proposes, with experimental rather than formal proof evidence, The observation in the first two lines is Pink contextual behavior; the last two demand the exact administrative-normal-form code, which is the claimed optimality. These are Propositions 4.2–4.6 of the source, where the authors state that formal proofs are absent [AR18].

This evidence has a hard boundary. The source supplies experiments rather than a proof of the claimed contextual equations, so it does not prove $$\mathsf{run}(\mathsf{collapse}(J,I,p)){\approx }_{\mathsf{tower}}J⌜I⌝⌜p⌝.$$ Accordingly, no tower-collapse theorem appears in this chapter’s theorem ledger.

Sources and seminar

The principal calculus, its dual-context proofs, and the two-level embedding are those of Davies and Pfenning [DP01]. The staged-reference and tower cards are intentionally source-bounded [TW26, AR18]. No public theorem from those cards transfers to the modal calculus by notation alone.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 129.3, then complete exercise 129.8.

Exercise 129.3¶

★★☆ Construct a boxed exponentiation generator for exponent four. Give every context in its derivation, reduce the generator to a code value, and type the code body under the empty ordinary context.

Referenced from 4 locations

• Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
• ch:typed-staging: ch:typed-staging

Exercise 129.4¶

★★☆ Extend the term grammar with references and propose unrestricted CSP. Exhibit a reference that outlives its allocation stage. State a value restriction that blocks this term; do not claim preservation for the extension.

Referenced from 3 locations

• Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
• ch:typed-staging: ch:typed-staging

Exercise 129.5¶

★★☆ For a fixed dimension two, construct a generator for matrix multiplication whose input entries are modal naturals. Derive the code type of one output entry, then display the four output entries. State the exact point at which unknown dimensions would require dependent types absent from $\mathsf{Tstage}$.

Referenced from 3 locations

• Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
• ch:typed-staging: ch:typed-staging

Exercise 129.6¶

★★☆ Let generators $G_1,G_2$ each append their name to a stage-zero log and return boxed naturals. Calculate the logs produced by left-to-right let insertion and by the reordered nesting. Repair the latter so that it produces the former log and the same residual addition.

Referenced from 3 locations

• Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
• ch:typed-staging: ch:typed-staging

Exercise 129.7¶

★★★ Fix object terms $p:\mathsf{nat}$, an interpreter $I:\mathsf{Code}\mathsf{nat}\to \mathsf{nat}$, and a meta-interpreter $J:\mathsf{Code}(\mathsf{Code}\mathsf{nat}\to \mathsf{nat})\to \mathsf{Code}\mathsf{nat}\to \mathsf{nat}$. Type the finite expression $J⟨I⟩⟨p⟩$. Identify which type is missing for an additional interpreter level and explain why this typing calculation proves no tower-collapse equation.

Referenced from 3 locations

• Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
• ch:typed-staging: ch:typed-staging

Exercise 129.8 — Practical: modal stage checker¶

★★★ Practical project.tstage-code-checker Implement in Agda or Kappa a finite checker for the six rule families, modal substitution beneath nested let-box, index decrement and contraction, and exponentiation. Require boxed-modal acceptance, boxed-ordinary rejection, results $7$ and $27$, and accepted index decrement. Implement the five-rule binding-time card with static and dynamic prints. Replay the ordinary-capture, index-decrement, and static-addition mutants; name respectively the missing T-Box premise, violated substitution invariant, and broken static-operator equation. The model makes no tower or effect claim.

Referenced from 5 locations

• Typed Multi-Stage Programming and an Evidence-Bounded Interpreter-Tower Case Study
• Specialization and staging: executable records
• ch:typed-staging: modal code checking