Dependent Closure Conversion for the Calculus of Constructions
Prerequisites. Direct starred prerequisites: Chapter 133 and chapter 26. No later core chapter depends on this route.
Closure conversion in chapter 133 hid the environment behind an existential. The reason that worked is that a simply typed function’s type mentions nothing from its environment. In the calculus of constructions it does.
Take the polymorphic identity, written with the two abstractions separated: 𝜆𝐴:⋆.𝜆𝑥:𝐴.𝑥. Converting the inner abstraction produces code whose environment holds 𝐴, so the code’s argument type must say “the first component of the environment”: ⟨⟨𝜆(𝑛2:⋆×𝟏,𝑥:𝖿𝗌𝗍𝑛2).𝑥,⟨𝐴,⟨⟩⟩⟩⟩. Now hide the environment type behind an existential, as one must for two closures of the same type with different environments to be interchangeable. The code’s type becomes Π(𝑛2:𝛼2,𝑥:𝖿𝗌𝗍𝑛2).𝖿𝗌𝗍𝑛2. Read that type: it projects the first component of something whose type is the abstract variable 𝛼2. Projection applies to pairs, and 𝛼2 is not a pair. The type is not well formed. Hiding the environment to recover type preservation has destroyed type preservation.
This chapter reconstructs the solution of Bowman and Ahmed (2018): abandon the existential, add primitive code and closure forms to the target, and give closures an equivalence principle strong enough that the translation of a Π type is the Π type of the translations.
Universes are 𝑈::=⋆∣◻, with ⋆ impredicative and ◻ predicative. Expressions are 𝑒,𝐴,𝐵::=𝑥∣⋆∣𝜆𝑥:𝐴.𝑒∣𝑒1𝑒2∣Π𝑥:𝐴.𝐵∣𝗅𝖾𝗍𝑥=𝑒:𝐴𝗂𝗇𝑒′∣Σ𝑥:𝐴.𝐵∣⟨𝑒1,𝑒2⟩∣𝖿𝗌𝗍𝑒∣𝗌𝗇𝖽𝑒. Reduction Γ⊢𝑒:⟶𝑒′ has the clauses 𝑥⟶𝑒when𝑥=𝑒:𝐴∈Γ(𝛿),(𝜆𝑥:𝐴.𝑒1)𝑒2⟶𝑒1[𝑒2/𝑥](𝛽),𝗅𝖾𝗍𝑥=𝑒:𝐴𝗂𝗇𝑒1⟶𝑒1[𝑒/𝑥](𝜁),𝖿𝗌𝗍⟨𝑒1,𝑒2⟩⟶𝑒1(𝜋1), and 𝗌𝗇𝖽⟨𝑒1,𝑒2⟩⟶𝑒2. Equivalence Γ⊢𝑒1≡𝑒2 holds when both reduce to a common expression, or by either 𝜂 rule: if 𝑒1⟶∗𝜆𝑥:𝐴.𝑒, 𝑒2⟶∗𝑒′2 and Γ,𝑥:𝐴⊢𝑒≡𝑒′2𝑥, then Γ⊢𝑒1≡𝑒2, and symmetrically.
Conv is what makes the rest of this chapter possible: a term keeps its type up to reduction, so a translation may produce a type that merely reduces to the intended one.
The standard translation for simply typed and polymorphic languages sets (Π𝑥:𝐴.𝐵)+=∃𝛼:𝑈.∃𝑛:𝛼.𝖢𝗈𝖽𝖾(𝑛′:𝛼,𝑦:𝑛′=𝑛,𝑥:𝐴+).𝐵+, quantifying over the environment’s type 𝛼 and value 𝑛, and giving the code a proof 𝑦 that it receives exactly 𝑛. Packing copies the witness into the type, so a closure 𝗉𝖺𝖼𝗄⟨𝐴′,𝑣,𝑒⟩ type-checks when 𝑒 has the type above with 𝑛′ replaced by 𝑣.
Suppose construction 137.3 is type preserving. Then for every 𝐴,𝐵 with Γ⊢Π𝑥:𝐴.𝐵:⋆, the type ∃𝛼:𝑈.… also has type ⋆. Since 𝑈 ranges over both universes, the existential quantifier must be impredicative.
Proof of Proposition 137.4 — The existential encoding needs impredicativity
Proof. Type preservation requires (Π𝑥:𝐴.𝐵)+ to inhabit the translation of the universe of Π𝑥:𝐴.𝐵, which is ⋆. The environment of a closure may contain a type, so 𝛼 may be instantiated at ◻; a quantifier over ◻ whose result lies in ⋆ is impredicative by definition. ◻
That is not an idle restriction. A computationally relevant universe is predicative in the default configuration of the proof assistant this calculus models, impredicativity at more than one relevant universe is unsound, and some dependently typed languages admit none at all. A second obstruction is independent of the first: an 𝜂 principle for existentially packaged closures would have to be justified by a parametric relation on environments, and dependent type theories do not all admit parametricity.
For System F the repair is to add singleton types, type-level pairs and kinds, so that the environment’s type can be described precisely enough to project from. Every one of those features is encodable in CC, so the repair transfers syntactically — and proposition 137.4 still applies, because the existential is still there. A different repair for System F erases types before run time, so code need not close over type variables; in CC types contain term variables, and there is nothing to erase.
First, Code types its body in the empty context. That single premise is the entire content of typed closure conversion: it is a machine-checked guarantee that the translation produces closed code, and it is checked by the target’s own type checker rather than by a metatheorem.
Second, Clo substitutes the environment into the closure’s type. A closure ⟨⟨𝑒,𝑒′⟩⟩ is therefore not a pair but a delayed partial application of 𝑒 to 𝑒′, and its type is computed exactly as dependent application computes the type of 𝑒𝑒′. Nothing is hidden, and nothing needs to be.
Third, the closure type is an ordinary Π type. There is no new type former for closures, so the translation of a source Π has somewhere to go.
Type checking in CC reduces terms. Two syntactically identical closures can become distinct when reduction inlines a term into one environment and not the other, and a naive syntactic comparison would then call them inequivalent. Definition 137.7 removes the possibility by never comparing environments at all: it inlines both and compares the resulting bodies with the argument left free. A consequence is a normal form for closures in which the environment is a tuple of variables.
Write FV(𝑒,Γ)=𝑥1:𝐴1,… for the free variables of 𝑒 in Γ, ordered so that each 𝐴𝑖 mentions only earlier ones. Then (Π𝑥:𝐴.𝐵)+=Π𝑥:𝐴+.𝐵+,(𝜆𝑥:𝐴.𝑒)+=⟨⟨𝜆(𝑛:Σ(𝑥𝑖:𝐴+𝑖…),𝑥:𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐴+).𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝑒+,⟨𝑥𝑖…⟩⟩⟩, where 𝑥𝑖:𝐴𝑖⋯=FV(𝜆𝑥:𝐴.𝑒,Γ); every other form translates componentwise.
The first clause is the surprise. The translation of a dependent function type is the dependent function type of the translations — exactly as if nothing had happened. The next lemma says why that is consistent with definition 137.6.
Write 𝐴𝑥 for 𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐴+, let 𝑒code=𝜆(𝑛:𝐴𝑛,𝑥:𝐴𝑥).𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝑒+, and let 𝑣=⟨𝑥𝑖…⟩. Then Clo gives the closure ⟨⟨𝑒code,𝑣⟩⟩ the type Π𝑥:(𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐴+)[𝑣/𝑛].(𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐵+)[𝑣/𝑛], and that type reduces by 𝜋1, 𝜋2 and 𝜁 steps to Π𝑥:𝐴+.𝐵+.
Proof of Lemma 137.10 — The closure's type reduces to the translated type
Proof. Substituting 𝑣=⟨𝑥𝑖…⟩ for 𝑛 turns each 𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐶 into 𝗅𝖾𝗍⟨𝑥𝑖…⟩=⟨𝑥𝑖…⟩𝗂𝗇𝐶. Destructuring a literal tuple is |𝑖| projections followed by |𝑖|𝜁 steps, each binding 𝑥𝑖 to itself, so the result is 𝐶 with each 𝑥𝑖 replaced by 𝑥𝑖: that is 𝐶. Applying this to 𝐴+ and to 𝐵+ gives the claim. ◻
So Conv closes the gap between the type Clo assigns and the type definition 137.9 declares, and the declared type mentions no environment. Two closures of the same source type have the same target type whatever their environments contain, which is what the existential was for.
The inner closure of 𝜆𝐴:⋆.𝜆𝑥:𝐴.𝑥 is ⟨⟨𝜆(𝑛:Σ(𝐴:⋆),𝑥:𝗅𝖾𝗍⟨𝐴⟩=𝑛𝗂𝗇𝐴).𝗅𝖾𝗍⟨𝐴⟩=𝑛𝗂𝗇𝑥,⟨𝐴⟩⟩⟩. Its code is closed and type-checks by Code. By Clo its type is Π𝑥:(𝗅𝖾𝗍⟨𝐴⟩=⟨𝐴⟩𝗂𝗇𝐴).(𝗅𝖾𝗍⟨𝐴⟩=⟨𝐴⟩𝗂𝗇𝐴), which reduces to Π𝑥:𝐴.𝐴 by lemma 137.10. Compare the opening: there the type contained 𝖿𝗌𝗍𝑛2 with 𝑛2 of an abstract type, and no reduction was possible.
★★☆ Translate the outer abstraction of example 137.11 and give the resulting nested closure in full, together with the type Clo assigns to it and the type it reduces to. Say which free variable each environment contains and why the outer one is empty.
Proof. Induction on 𝑒1. The case that is not immediate is the abstraction, and it is the reason the lemma is the technical heart of the proof: substituting before translating changes which variables are free, hence the shape of the environment. Let 𝑒1=𝜆𝑦:𝐴.𝑒 with FV(𝑒1,Γ)=𝑥𝑖:𝐴𝑖…. If 𝑥 is not among the 𝑥𝑖, both sides build the same environment and the induction hypothesis applies componentwise. If 𝑥=𝑥𝑗, then substituting first removes 𝑥𝑗 from the free variables and inserts FV(𝑒2,Γ); substituting afterwards leaves the environment ⟨𝑥𝑖…⟩ with 𝑥𝑗 replaced by 𝑒+2. The two results differ syntactically, and definition 137.7 identifies them: both closures have the same code up to inlining the environment, and inlining is exactly what the equivalence rule performs. The statement is therefore proved up to ≡, which is all the later uses require. ◻
Proof. Most clauses of definition 137.1 are defined by substitution, so lemma 137.12 does the work. The 𝛽 case is the one that is not. The translation of (𝜆𝑥:𝐴.𝑒1)𝑒2 applies a closure to the translation of 𝑒2, and by definition 137.6 that reduces to (𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝑒+1)[⟨𝑥𝑖…⟩/𝑛][𝑒+2/𝑥]. By |𝑖|𝜁 steps that is 𝑒+1[𝑒+2/𝑥], which by lemma 137.12 is (𝑒1[𝑒2/𝑥])+. ◻
Proof. Induction on the equivalence derivation. The common-reduct case is lemma 137.13. The 𝜂 cases are where definition 137.7 is needed. Suppose 𝑒⟶∗𝜆𝑥:𝐴.𝑒1, 𝑒′⟶∗𝑒2 and Γ,𝑥:𝐴⊢𝑒1≡𝑒2𝑥. By lemma 137.13, 𝑒+ reduces to something equivalent to (𝜆𝑥:𝐴.𝑒1)+ and 𝑒′+ to something equivalent to 𝑒+2, so by transitivity it suffices to relate those two. Rule ≡-Clo1 reduces that obligation to 𝗅𝖾𝗍⟨𝑥𝑖…⟩=⟨𝑥𝑖…⟩𝗂𝗇𝑒+1≡𝑒+2𝑥; the left side is 𝑒+1 after |𝑖|𝜁 steps, and the induction hypothesis applied to 𝑒1≡𝑒2𝑥 finishes. ◻
Lam. Let Γ⊢𝜆𝑥:𝐴.𝑒1:Π𝑥:𝐴.𝐵 with Γ,𝑥:𝐴⊢𝑒1:𝐵, and let 𝑥𝑖:𝐴𝑖… be the free variables of 𝑒1, 𝐴 and 𝐵. The induction hypothesis at Γ⊢𝐴:𝑈, weakened, gives 𝑛:Σ(𝑥𝑖:𝐴+𝑖…)⊢𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐴+:𝑈+. The induction hypothesis at Γ,𝑥:𝐴⊢𝑒1:𝐵, weakened, gives ⋅,𝑛,𝑥⊢𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝑒+1:𝗅𝖾𝗍⟨𝑥𝑖…⟩=𝑛𝗂𝗇𝐵+ — the context is empty because 𝑥𝑖… are all the free variables, which is the premise Code demands. So Code types the code, Clo types the closure, and lemma 137.10 together with Conv moves that type to Π𝑥:𝐴+.𝐵+=(Π𝑥:𝐴.𝐵)+.
App. Let Γ⊢𝑒1𝑒2:𝐵[𝑒2/𝑥]. By lemma 137.12 it suffices to show Γ+⊢𝑒+1𝑒+2:𝐵+[𝑒+2/𝑥], which is App in the target applied to the two induction hypotheses, since 𝑒+1 has type Π𝑥:𝐴+.𝐵+ by the hypothesis at 𝑒1.
Conv.Lemma 137.14 transports the equivalence, and Conv in the target reapplies. The remaining rules translate componentwise. ◻
Consistency of the target
Adding typing rules to a dependent type theory is adding axioms to a logic. Definition 137.6 must therefore be shown consistent, and shown not to lose any proof the source had.
Define ⋅∘ from CC-CC to CC by erasing the primitive forms: 𝖢𝗈𝖽𝖾(𝑥′:𝐴′,𝑥:𝐴).𝐵 becomes Π𝑥′:𝐴′∘.Π𝑥:𝐴∘.𝐵∘, the code abstraction becomes the corresponding double abstraction, and ⟨⟨𝑒,𝑒′⟩⟩ becomes 𝑒∘𝑒′∘.
Proof of Theorem 137.18 — Consistency and type safety of CC-CC
Proof. For consistency: the back-translation preserves typing — Clo becomes App because the closure’s type is the application’s type, and Code becomes two Lam steps — and preserves equivalence, including the closure rule of definition 137.7, which becomes the 𝜂 rule of definition 137.1 after the two applications are performed. A closed CC-CC proof of 𝖥𝖺𝗅𝗌𝖾 would therefore back-translate, by lemma 137.17, to a closed CC proof of 𝖥𝖺𝗅𝗌𝖾, and CC has none. Type safety follows from the same transport together with normalization for CC. ◻
Two transports are needed and they do different work. Theorem 137.15 goes forwards and says the compiler produces well-typed target code. Theorem 137.18 goes backwards and says the target’s new rules prove nothing the source could not. A translation could satisfy the first with an inconsistent target, in which case the target’s type checker would accept everything.
A component is a well-typed open term Γ⊢𝑒:𝐴. Linking is substitution by a closing substitution 𝛾 with Γ⊢𝛾 when ⋅⊢𝛾(𝑥):𝐴 for every 𝑥:𝐴∈Γ. The compiler is extended to substitutions pointwise. Fix a ground type with a relation 𝑣≈𝑣′ on its values — for booleans, 𝗍𝗋𝗎𝖾≈𝗍𝗋𝗎𝖾 and 𝖿𝖺𝗅𝗌𝖾≈𝖿𝖺𝗅𝗌𝖾.
Proof of Theorem 137.21 — Correctness of separate compilation
Proof. The square (𝛾(𝑒))+≡𝛾′(𝑒+)≡≡𝑣+≡𝑣′ commutes. The top edge is lemma 137.12 together with the hypothesis 𝛾+≡𝛾′ and lemma 137.14. The left edge is lemma 137.13 applied to 𝛾(𝑒)⟶∗𝑣; the right edge is reduction of 𝛾′(𝑒+), which terminates by theorem 137.18. Transitivity of ≡ gives 𝑣+≡𝑣′, and at a ground type equivalence implies ≈. ◻
★★☆ Show that theorem 137.21 becomes false if “𝐴 ground” is dropped, by exhibiting a source component of function type whose translation is equivalent to, but not observationally identical to, the translation of its value. Then say which step of the proof used groundness.
★☆☆ Delete the emptiness of the context from the premise of Code and give a target term that becomes well typed and whose code is not closed. Say which sentence of section 137.3 that premise was carrying.
Five boundaries. The source is the calculus of constructions with Σ types and 𝜂; there are no inductive types, so this is not a translation for the calculus of inductive constructions and nothing here covers pattern matching, fixed points or universe polymorphism. Only one compiler pass is treated: there is no continuation-passing pass before it and no allocation pass after it, and theorem 137.21 is about this pass alone. Theorem 137.21 is stated at ground types, so it says nothing about components whose interface is a function type; a compositional statement would need a relation between source and target components chosen independently of the compiler. The equivalence of definition 137.7 is presented declaratively here and its algorithmic form is what a checker would implement; decidability of the target’s conversion is claimed by the source and not proved here. Finally, the target is a high-level dependently typed language, not assembly: theorem 137.18 guarantees safety of linking any two well-typed CC-CC components, and says nothing about machine code.
[4]
Suggested first pass.
None of these problems is a prerequisite for a later chapter. Begin with exercise 137.4, then complete exercise 137.7.
★★★ Carry construction 137.3 through on 𝜆𝐴:⋆.𝜆𝑥:𝐴.𝑥, writing every type in full, and identify the first judgment that is underivable. Then add singleton types and type-level pairs as in remark 137.5, redo the derivation, and locate the step that requires impredicativity.
★★★ Give two closures with the same code but environments that reduction has inlined differently, show that they are not syntactically equal, and derive their equivalence with ≡-Clo. Then show that deleting that rule makes lemma 137.14 false, by exhibiting a source equivalence whose translation is no longer derivable.
★★★Practical project.dcc-closure-checker Complete project dcc-closure-checker. Implement, for the fragment of CC with ⋆, variables, dependent functions, application and Σ types with projections, (i) a type checker for CC and one for CC-CC including Code, Clo and Conv, (ii) reduction to weak head normal form for both, and (iii) the translation of definition 137.9 together with the free-variable sequence. The invariant the implementation must maintain is theorem 137.15 on every accepted input: a term accepted by the CC checker at type 𝐴 must translate to a term accepted by the CC-CC checker at 𝐴+. The named cases print
polymorphic-identity: accepted
closure-type-reduces: ok
open-code: rejected
existential-projection: rejected
type-preserved: ok
The checker is independent evidence on the named inputs; it does not prove theorem 137.15, implements neither definition 137.7 beyond reduction to a common form nor the back-translation of construction 137.16, and establishes nothing about theorem 137.18 or theorem 137.21. If the environment is built as a right-nested pair, record whether the implementation handles a component whose type mentions an earlier component; if it does not, include a source term with such an environment among the named inputs and check that the translation declines it, so that the restriction is visible rather than silent.