Prerequisites. Direct starred prerequisites: Chapter 137. No later core chapter depends on this route.
A compiler that wants a machine-like intermediate language names every intermediate computation. The expression 𝑓(𝗌𝗇𝖽𝑒) becomes a sequence of primitive steps, 𝗅𝖾𝗍𝑦=𝑒𝗂𝗇𝗅𝖾𝗍𝑧=𝗌𝗇𝖽𝑦𝗂𝗇𝑓𝑧, and in a simply typed language that is the end of the matter. With dependent types it is not. Let 𝑒:Σ𝑥:𝐴.𝐵, so that 𝗌𝗇𝖽𝑒:𝐵[𝖿𝗌𝗍𝑒/𝑥], and let 𝑓:𝐵[𝖿𝗌𝗍𝑒/𝑥]→𝐶. In the sequence above, 𝗌𝗇𝖽𝑦 has type 𝐵[𝖿𝗌𝗍𝑦/𝑥], because the typing rule for the second projection copies its own scrutinee into the type. The scrutinee is now the variable 𝑦, not 𝑒. So 𝑓 is applied to an argument of the wrong type, and the ANF term does not type check — although the original does, and although the two compute the same thing.
The same failure appears for positive types. If 𝑓(𝐢𝐟𝑒𝐭𝐡𝐞𝐧𝑒1𝐞𝐥𝐬𝐞𝑒2) is well typed with 𝑓:𝐵[𝑒/𝑥]→𝐶 and 𝑒1:𝐵[𝗍𝗋𝗎𝖾/𝑥], then pushing 𝑓 into the branches applies it to an argument of type 𝐵[𝗍𝗋𝗎𝖾/𝑥], and the type system cannot know that 𝑒 equals 𝗍𝗋𝗎𝖾 in that branch.
Both failures have one cause. By the time the machine runs the body of the 𝗅𝖾𝗍, it has performed the step 𝑦=𝑒; by the time it runs a branch, it has evaluated 𝑒 to a boolean. The type system has no way to record either fact. This chapter follows Koronkevich, Rakow, Ahmed and Bowman (2022): give the target two ways to record a performed machine step, and the ANF translation preserves dependent types — up to an equality that the target must be able to reflect.
The source is the extended calculus of constructions: dependent functions Π𝑥:𝐴.𝐵, dependent pairs Σ𝑥:𝐴.𝐵 with projections, booleans with dependent 𝐢𝐟, a predicative universe hierarchy, and definitional equality ≡ containing 𝛽, 𝜂 and 𝜁. The two dependent elimination rules that matter are
Target expressions are stratified into values, computations and configurations: 𝑉::=𝑥∣𝗍𝗋𝗎𝖾∣𝖿𝖺𝗅𝗌𝖾∣𝜆𝑥:𝐴.𝑀∣⟨𝑉,𝑉⟩∣Π𝑥:𝐴.𝐵∣Σ𝑥:𝐴.𝐵∣𝖡𝗈𝗈𝗅∣𝖳𝗒𝗉𝖾𝑖,𝑁::=𝑉∣𝑉1𝑉2∣𝖿𝗌𝗍𝑉∣𝗌𝗇𝖽𝑉,𝑀::=𝑁∣𝗅𝖾𝗍𝑥=𝑁𝗂𝗇𝑀∣𝐢𝐟𝑉𝐭𝐡𝐞𝐧𝑀1𝐞𝐥𝐬𝐞𝑀2. A configuration is a sequence of let-bound primitive computations ending in a computation or a branch; no 𝗅𝖾𝗍 is nested inside another’s bound computation. The machine reduces the leftmost binding, whose operands are already values.
The highlighted change is the context entry. In the standard rule the definition appears only in the substitution performed on the output type; here it is available while checking the body, which is exactly where the opening’s failure occurred.
With definition 138.3 the sequence 𝗅𝖾𝗍𝑦=𝑒𝗂𝗇𝗅𝖾𝗍𝑧=𝗌𝗇𝖽𝑦𝗂𝗇𝑓𝑧 type-checks. Checking the inner body proceeds under 𝑦𝛿=𝑒:Σ𝑥:𝐴.𝐵, so 𝐵[𝖿𝗌𝗍𝑦/𝑥]≡𝐵[𝖿𝗌𝗍𝑒/𝑥] by 𝜁, and 𝑓 may be applied to 𝑧. The definitional equality that Let makes available is precisely the machine step the type system had forgotten.
★☆☆ Delete the context entry from Let, keeping the substitution in the conclusion, and show that example 138.4 no longer type-checks. Name the equivalence step that becomes underivable.
Pushing 𝑓:𝐵[𝑒/𝑥]→𝐶 into the two branches now type-checks. In the true branch the context contains 𝑝:(𝑒≡𝗉𝗋𝗈𝗉𝗍𝗋𝗎𝖾), so ≡-Reflect gives 𝑒≡𝗍𝗋𝗎𝖾 and hence 𝐵[𝑒/𝑥]≡𝐵[𝗍𝗋𝗎𝖾/𝑥]; the argument 𝑒1 has the latter type and 𝑓 expects the former. The false branch is the same with 𝖿𝖺𝗅𝗌𝖾.
Definition 138.3 is a conservative extension: definitions are admissible in any pure type system, and proof assistants already have them. Definition 138.5 is not. ≡-Reflect is equality reflection, and a type theory with equality reflection has undecidable type checking: deciding Γ⊢𝑒1≡𝑒2 requires deciding whether some 𝑝 inhabits 𝑒1≡𝗉𝗋𝗈𝗉𝑒2, which is a proof search. The target is therefore an extensional calculus, suitable as a specification of what the translation preserves and not as a checker. Recovering decidability means restricting where reflection may be used — for instance to the equalities the translation itself introduces — and that restriction is not developed here.
★★☆ Show that ≡-Reflect makes Γ⊢𝑒1≡𝑒2 as hard as inhabitation of 𝑒1≡𝗉𝗋𝗈𝗉𝑒2. Then propose a syntactic restriction on the rule that suffices for example 138.6 and say which of the chapter’s later lemmas would have to be rechecked under it.
The translation is indexed by a continuation — a configuration with a hole — and the type of its output is known only once the hole is filled. The metatheory therefore needs a typing judgment for continuations.
The judgment records the term 𝑁 the hole is expected to receive, because the body’s type may depend on it; the side condition 𝑥∉fv(𝐵) makes the result type independent of the hole, so that continuations compose.
Proof. By cases on the continuation typing derivation. For K-Empty the plugged term is 𝑁 and 𝐵=𝐴. For K-Let the plugged term is 𝗅𝖾𝗍𝑥=𝑁𝗂𝗇𝑀; the premise gives Γ,𝑥𝛿=𝑁:𝐴⊢𝑀:𝐵, so Let types it at 𝐵[𝑁/𝑥], which is 𝐵 because 𝑥∉fv(𝐵). ◻
Proof of Lemma 138.10 — Continuation cut modulo equivalence
Proof. By cases on 𝐾. K-Empty is immediate. For 𝐾=𝗅𝖾𝗍𝑥=[]𝗂𝗇𝑀 it suffices to show that Γ,𝑥𝛿=𝑁:𝐴⊢𝑀:𝐵 implies Γ,𝑥𝛿=𝑁′:𝐴⊢𝑀:𝐵. The only use a derivation can make of the entry 𝑥𝛿=𝑁:𝐴 is a 𝜁 step 𝐶≡𝐶[𝑁/𝑥]. Replace each such step by 𝐶≡𝐶[𝑁′/𝑥]≡𝐶[𝑁/𝑥], the second equivalence following from 𝑁≡𝑁′ because substitution respects equivalence. Every other step of the derivation is unchanged. ◻
Building equivalence into definition 138.8 — typing 𝐾 against any 𝑁′≡𝑁 — would make continuation typing correct but would spoil its induction principle, because the inversion of K-Let would no longer determine the recorded term. Lemma 138.9, Lemma 138.10 together say that continuation typing is admissible rather than an extension: plugging a well-typed computation into a well-typed continuation always yields a well-typed configuration of the expected type.
Write [[𝑒]]𝐾 for the translation of 𝑒 with continuation 𝐾. A value translates by filling the hole; a computation translates by naming its subterms. The two clauses that matter are [[𝗌𝗇𝖽𝑒]]𝐾=[[𝑒]](𝗅𝖾𝗍𝑥=[]𝗂𝗇𝐾⟨𝗌𝗇𝖽𝑥⟩),[[𝑒1𝑒2]]𝐾=[[𝑒1]](𝗅𝖾𝗍𝑥1=[]𝗂𝗇[[𝑒2]](𝗅𝖾𝗍𝑥2=[]𝗂𝗇𝐾⟨𝑥1𝑥2⟩)), and the whole-program translation is [[𝑒]]=[[𝑒]][].
Proof of Theorem 138.13 — The output is in A-normal form
Proof. Induction on 𝑒. Every clause either fills the hole of 𝐾 with a value or a primitive computation, or calls the translation recursively with a continuation of the form 𝗅𝖾𝗍𝑥=[]𝗂𝗇𝑀; neither places a 𝗅𝖾𝗍 inside the bound computation of another. ◻
The type-preservation statement is not provable as it stands, and the reason is worth seeing before the repair.
Consider [[𝗌𝗇𝖽𝑒]]𝐾. The induction hypothesis for “Γ⊢𝑒:𝐴 implies [[Γ]]⊢[[𝑒]]:[[𝐴]]” tells us about [[𝑒]][], not about [[𝑒]] applied to the newly built continuation 𝗅𝖾𝗍𝑥=[]𝗂𝗇𝐾⟨𝗌𝗇𝖽𝑥⟩. The hypothesis must carry typing information for whatever continuation the clause constructs.
Proof of Lemma 138.15 — Type preservation, strengthened
Proof. Induction on the source typing derivation.
Snd. Let Γ⊢𝑒:Σ𝑥:𝐴.𝐵, so that 𝗌𝗇𝖽𝑒:𝐵[𝖿𝗌𝗍𝑒/𝑥], and let 𝐾 be typed at ([[𝗌𝗇𝖽𝑒]]:[[𝐵[𝖿𝗌𝗍𝑒/𝑥]]])⇒𝐶. Apply the induction hypothesis at 𝑒 with the continuation 𝐾′=𝗅𝖾𝗍𝑦=[]𝗂𝗇𝐾⟨𝗌𝗇𝖽𝑦⟩. Typing 𝐾′ by K-Let requires Γ,Γ′,𝑦𝛿=[[𝑒]]:[[Σ𝑥:𝐴.𝐵]]⊢𝐾⟨𝗌𝗇𝖽𝑦⟩:𝐶. In that context 𝑦≡[[𝑒]] by 𝜁, hence [[𝐵[𝖿𝗌𝗍𝑦/𝑥]]]≡[[𝐵[𝖿𝗌𝗍𝑒/𝑥]]], so 𝗌𝗇𝖽𝑦 has the type the hole of 𝐾 expects up to equivalence, and lemma 138.10 gives the required judgment. The induction hypothesis then types [[𝑒]]𝐾′=[[𝗌𝗇𝖽𝑒]]𝐾 at 𝐶.
Application. The same argument twice, with the inner continuation typed under the definition of 𝑥1 and the outer one under the definitions of both.
If𝛿. The continuation is duplicated into the two branches. In the true branch the context acquires 𝑝:([[𝑒]]≡𝗉𝗋𝗈𝗉𝗍𝗋𝗎𝖾), and ≡-Reflect makes [[𝐵[𝑒/𝑥]]] equivalent to [[𝐵[𝗍𝗋𝗎𝖾/𝑥]]], which is what the duplicated continuation needs; the false branch is symmetric. Without definition 138.5 this case is where the proof stops.
The value and remaining computation cases fill the hole directly and appeal to lemma 138.9. ◻
The first half says the compiler is compositional: translating a term and then placing it in a context is translating it in the composed context. The second half is what makes the source’s substitution match the target’s, and it is the step that turns theorem 138.16 into a statement about linking.
The target is consistent
Adding definition 138.5 and ≡-Reflect to a type theory is adding axioms. The target must be shown to prove nothing new.
Define [[⋅]]M from the target back to the source by erasing the recorded equality: an 𝐢𝐟 with its proof binder becomes the source 𝐢𝐟, a use of ≡-Reflect becomes the corresponding source equivalence, and a definition becomes a 𝗅𝖾𝗍.
Proof of Theorem 138.20 — Consistency and subject reduction
Proof. Consistency: a closed target proof of ⊥ would be sent by lemma 138.19 to a closed source proof of ⊥, and the source has none. Subject reduction reduces to the single-step case. That case needs context replacement, which says that a derivation is unchanged when a context entry is replaced by an equivalent one, and it needs the two cut lemmas, for variables and for definitions. Each is proved by induction on the derivation, replacing every use of the affected entry as in lemma 138.10. ◻
Proof. Each machine step is a 𝛽, 𝜁 or projection step, hence an equivalence; iterate, using naturality of continuation plugging to move the step under the surrounding configuration. ◻
Let Γ⊢𝑒:𝐴 with 𝐴 a base type, let 𝛾 be a closing substitution for Γ, and let 𝛾′ be a target closing substitution with [[𝛾]]≡𝛾′. Then eval(𝛾(𝑒))andeval(𝛾′([[𝑒]]))arethesamebasevalue.
Proof of Theorem 138.22 — Correctness of separate compilation
Proof. The square eval(𝛾(𝑒))≡𝛾(𝑒)≡≡eval(𝛾′([[𝑒]]))≡𝛾′([[𝑒]]) commutes: the horizontal edges are theorem 138.21 in the source and in the target, the right edge is lemma 138.17 together with the hypothesis on 𝛾′, and the left edge follows. At a base type, equivalence of two values is equality of those values. ◻
The restriction to base types is not decoration. At a function type, equivalence of the two results is not the same as their being the same value, and the theorem would need a relation between source and target values chosen independently of the compiler.
★★☆ Exhibit a source term of function type for which the conclusion of theorem 138.22, read as “the same value”, is false while the equivalence still holds. Then say which line of the proof used the base-type hypothesis.
Definition 138.12 copies the continuation into both branches of an 𝐢𝐟. A source term with 𝑛 nested conditionals in the argument position of a continuation therefore has a translation of size exponential in 𝑛.
Proof of Proposition 138.23 — The translation duplicates code
Proof. Let 𝐶𝑛 be the size of the translation of 𝑛 nested conditionals with a continuation of size 𝑘. The clause for 𝐢𝐟 places a copy of the continuation in each branch, so 𝐶𝑛≥2𝐶𝑛−1 and 𝐶0≥𝑘; hence 𝐶𝑛≥2𝑛𝑘. ◻
Bind the continuation once, as a function taking the branch result and the recorded equality, and call it from both branches: Write 𝑊 for [[𝐢𝐟𝑒𝐭𝐡𝐞𝐧𝑒1𝐞𝐥𝐬𝐞𝑒2]] and 𝐾𝑖=𝗅𝖾𝗍𝑥𝑖=[]𝗂𝗇𝑓𝑥𝑖(𝗋𝖾𝖿𝗅𝑥𝑖). Then [[𝐢𝐟𝑒𝐭𝐡𝐞𝐧𝑒1𝐞𝐥𝐬𝐞𝑒2]]𝐾=𝗅𝖾𝗍𝑓=𝜆𝑦:[[𝐵[𝑒/𝑥]]].𝜆𝑝:(𝑦≡𝗉𝗋𝗈𝗉𝑊).𝐾⟨𝑦⟩𝗂𝗇[[𝑒]](𝗅𝖾𝗍𝑥=[]𝗂𝗇𝐢𝐟𝑥𝐭𝐡𝐞𝐧[[𝑒1]]𝐾1𝐞𝐥𝐬𝐞[[𝑒2]]𝐾2).
Proof of Lemma 138.25 — The join-point translation is type preserving
Proof. Only the 𝐢𝐟 case changes. The join point 𝑓 must be applied to arguments of the right types. For the first argument, in the true branch the context contains 𝑥1𝛿=[[𝑒1]], and [[𝐵[𝑒/𝑥]]]≡[[𝐵[𝗍𝗋𝗎𝖾/𝑥]]] by ≡-Reflect on the recorded equality, which is the equivalence already used in lemma 138.15. For the second, it suffices to show (𝑥1≡𝗉𝗋𝗈𝗉𝑥1)≡(𝑥1≡𝗉𝗋𝗈𝗉[[𝐢𝐟𝑒𝐭𝐡𝐞𝐧𝑒1𝐞𝐥𝐬𝐞𝑒2]]), which by congruence reduces to 𝑥1≡[[𝐢𝐟𝑒𝐭𝐡𝐞𝐧𝑒1𝐞𝐥𝐬𝐞𝑒2]], and that is the same equivalence again under the definition of 𝑥1. The false branch is symmetric. ◻
Construction 138.24 needs the type 𝐵 of the branch, which the source 𝐢𝐟 does not carry. Either define the translation by induction on typing derivations, or annotate the source 𝐢𝐟 with 𝐵. The second is preferable and is what dependent case analysis in a proof assistant already does.
Five boundaries. The target’s type checking is undecidable, by remark 138.7: it is a specification of what ANF preserves, and a compiler that used it as an intermediate representation would need a restricted form of reflection that is not developed here. Theorem 138.22 holds at base types only. The source is the extended calculus of constructions with booleans and natural numbers; there are no general inductive types, no pattern matching and no fixed points, so nothing here covers a realistic dependent source language. The translation is one pass: there is no continuation-passing pass before it, no closure conversion after it, and no claim that the passes compose. Finally, the equality of theorem 138.16 is extensional — the target’s equivalence includes reflected propositional equalities — so “preserves dependent types” means preserves them up to that equality, and not up to the source’s definitional equality.
[4]
Suggested first pass.
None of these problems is a prerequisite for a later chapter. Begin with exercise 138.5, then complete exercise 138.8.
★★★ Give a source term whose translation needs bothdefinition 138.3 and definition 138.5, and show that deleting either one makes the translation ill typed. Identify the smallest such term you can.
★★★ Delete the side condition 𝑥∉fv(𝐵) from K-Let. Show that lemma 138.9 becomes false, and that continuations no longer compose; exhibit the two continuations whose composition has no type.
★★★Practical project.anf-dependency-checker Complete project anf-dependency-checker. Implement, for a source fragment with dependent pairs, projections, booleans and dependent 𝐢𝐟, (i) a type checker for the source, (ii) a type checker for the A-normal target including the definition-recording Let of definition 138.3 and the equality-recording If𝛿 of definition 138.5 with reflection restricted to the recorded equalities, and (iii) the two translations of a nest of conditionals, the duplicating one of definition 138.12 and the join-point one of construction 138.24, with a size measure on the results. The invariant the implementation must maintain is that the target checker accepts an A-normal term exactly when the rule that records the corresponding machine step is enabled; if the full translation is also implemented, strengthen the invariant to theorem 138.16 on every accepted input. The named cases print
snd-let: accepted
snd-let-without-definitions: rejected
if-push: accepted
if-push-without-equalities: rejected
join-point-size: linear
The checker is independent evidence on the named inputs. It does not prove theorem 138.16 or lemma 138.15, implements no model and therefore says nothing about theorem 138.20, and its reflection rule is the restricted one, not the unrestricted ≡-Reflect; a checker using the unrestricted rule would not terminate on every input, by remark 138.7.