Closure conversion, monomorphisation and type erasure implemented on a Quantitative Dependently Typed Lambda Calculus (typechecked here).

Input terms are all assumed to be type-correct and already elaborated.

To run: ghc --make Main && ./Main. Upon success, you should some output similar to this execution trace:

>> Performing monomorphisation of term @e@ where
	e ≡ let id :^ω ∀(A : U). (x : A) ⊸ A = λ(A :^0 U) : ((x : A) ⊸ A). λ(x :^1 A) : A. x in (id ℕ 0 :^1 ℕ, id 𝟏 () : ())

>>> Success!

let "id𝟏" :^ω (x : 𝟏) ⊸ 𝟏 = λ(x :^1 𝟏) : 𝟏. x in let "idℕ" :^ω (x : ℕ) ⊸ ℕ = λ(x :^1 ℕ) : ℕ. x in ("idℕ" 0 :^1 ℕ, "id𝟏" () : ())

>> Performing closure conversion on term @e'@ where
	e' ≡ let "id𝟏" :^ω (x : 𝟏) ⊸ 𝟏 = λ(x :^1 𝟏) : 𝟏. x in let "idℕ" :^ω (x : ℕ) ⊸ ℕ = λ(x :^1 ℕ) : ℕ. x in ("idℕ" 0 :^1 ℕ, "id𝟏" () : ())

>>> Success!

let clos0 :^ω (x : 𝟏) ⊸ 𝟏 = λ(x :^1 𝟏) : 𝟏. x in let clos1 :^ω (x : ℕ) ⊸ ℕ = λ(x :^1 ℕ) : ℕ. x in let "id𝟏" :^ω (x : 𝟏) ⊸ 𝟏 = clos0 in let "idℕ" :^ω (x : ℕ) ⊸ ℕ = clos1 in ("idℕ" 0 :^1 ℕ, "id𝟏" () : 𝟏)

The line under the first >>> Success! is the monomorphised term synthetised from the input term e. The line under the second >>> Success! is the term resulting from closure conversion of the monomorphised term.

---

Here's the list of available input terms:

• Type annotations (in the erased theory):
  • Π(x :ⁱ A). B is the dependent function type taking a value of type A as input and returning a value of type B (after consuming x).
  • (x :ⁱ A) ⊗ B is the multiplicative dependent pair type.
  • 𝟏 is the multiplicative unit type.
  • U is the type of types and universes (hence we have U :⁰ U)
• Expressions (with runtime presence):
  • λ(x :ᵖ A) :ⁱ B. e is a lambda expression taking a parameter of type A with usage p and returns the expression e with type B (usage is restricted to i).
  • x is a simple bound variable (type can be determined by examining binding points, e.g. parameters of lambda abstractions).
  • (a :ᵖ A, b : B) is the multiplicative dependent pair containing the value a of type A with usage p and the value b of type B.
  • () is the multiplicative unit value.
  • f x is the basic function application that all of us know.
  • let () as z = a in b is the common eliminator for the multiplicative unit. This evaluates a first and returns the result of evaluating b.
  • let x :ⁱ A = e in r locally binds the identifier x to the value of e (which is of type A) and returns the value of r (which may make use of x).
  • n denotes a common natural number (0, 2530, etc.).

---

Output terms are mostly the same as input terms, with a few variations:

• Type annotations:
  • @{ x :ⁱ A, y :ᵖ B, ... } is a record type with labels.
• Expressions:
  • @{ x :ⁱ A = e₁, y :ᵖ B = e₂, ... } is a literal record value where each label has a specific value.
  • let (x :ⁱ A, y :ⁱ B) as z = a in b is the destructor for the multiplicative dependent pair.
  • rec x :ᵖ A = e in r is a let binding which allows e to use x (x is allowed to reference itself in its value).
  • r.x is the record accessor, meaning that it returns the value at label x in the record r (assuming that it is present).

Records are necessary for closure conversion, to maintain the state of the closure (what each free variable is bound to when we are defining a lambda expression).