Created: 2017-12-13 ons 16:16
There are few descriptions of implementations of Agda-like languages with an emphasis of performance.
We aim to fill this gap.
Set
(x : A) → B : Set
Records:
record Sigma (A : Set) (B : A → Set) : Set where constructor pair field fst : A snd : B fst
data U : Set El : U → Set data U where set : U el : Set → U pi : (a : U) → (El a → U) → U El set = Set El (el A) = A El (pi a b) = (x : El a) → El (b x)
There is a built-in equality type with computational J.
_==_ : {A : Set} → (a b : A) → Set refl : (A : Set) → (a : A) → a == a J : (A : Set) → (x y : A) → (P : (x y : A) → (eq : x == y) → Set) → (p : (x : A) → P x x refl) → P x y eq
The user may omit some terms in their code:
data Bool : Set where true false : Bool id : {A : Set} → A → A; id x = x t = id true
Internally: (· ⊢ ?α : Set
, · ⊢ ?β : Set
)
id : (A : Set) → A → A; id _ a = a t : ?α t = id ?β true
Is this code type-correct?
data Bool : Set where true false : Bool id : (A : Set) → A → A; id _ a = a t : ?α t = id ?β true
More precisely, can we assign terms to ?α
and ?β
that
such that the above program is type-correct?
Yes! Θ = [?α ≔ Bool, ?β ≔ Bool]
.
The assignment Θ is a metasubstitution.
In general, metasubstitutions are solutions to unification problems.
Type-checking a program with metavariables
↔ solving its corresponding unification problem
(see [Mazzoli, Abel 2016])
Σ,Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
Σ,Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
Σ contains record/data/function declarations and definitions.
Θ is a metasubstitution containing both
metavariable declarations (?α : Set
) and
instantiations (?α ≔ Bool
).
Instantiations must respect the type of the meta.
Notation: Σ, Θ may be left implicit.
Σ, Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
Well-formed input constraints are of the form
Γ ⊢ t : A ≈ u : B
,
… where Γ ⊢ t : A
, Γ ⊢ u : B
.
If A=B
, we write Γ ⊢ t ≈ u : A
.
Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
For each constraint 𝒞ᵢ, we have an associated blocker ℬᵢ.
Unblocks when… ℬ := ?α, ?β ; ?α is instantiated | 𝒞̄₁,…,𝒞̄ₙ ; 𝒞̄ᵢ ↦ □ | d₁, d₂, … ; body for def. dᵢ is given | ℬ₁ ∧ ℬ₂ | ℬ₁ ∨ ℬ₂ ; ℬ₁ and/or ℬ₂ unblocks | ⊤ | ⊥ ; always/never
Σ,Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
𝒞 = Γ ⊢ t:A ≈ u:B
is a metasubstitution Θ
such that (Γ ⊢ t:A ≡ u:B)[Θ]
.Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
is a metasubstitution Θ’, such that:
We i) break the constraints into smaller ones
ii) until they give us the solution Θ’.
Figure 1: Σ,Θ; (ℬ₁| 𝒞₁)∧…∧(ℬₙ| 𝒞ₙ) ⤏* Σ,Θ’; □
cc-by-sa
We will define a unification relation (↦
).
Θ| 𝒞 ↦ (ℬ₁| 𝒟₁) ∧ … ∧ (ℬₙ| 𝒟ₙ); Θ’
The algorithm (⤏
) applies (↦
) to unblocked constraints.
Θ| 𝒞ᵢ ↦ (ℬ⃗|𝒟⃗); Θ’ ──────────────────────────────────────────────── Θ; …∧ (⊤| 𝒞ᵢ) ∧… ⤏ Θ++Θ’;…∧ (ℬ⃗|𝒟⃗) ∧…
Notation: 𝒞 ↦ (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)
.
When n=0
, we write 𝒞 ↦ □
.
Θ| 𝒞 ↦ (ℬ⃗|𝒟⃗); Θ’
, where 𝒞 = Γ ⊢ t:A ≈ u:B
t≡u
are syntactically equal, we are done: 𝒞 ↦ □
.t := λt ; λ-abs. | x e* ; var. app. | c t* ; cons. | α e* ; meta. app. | T t* ; type cons. | d e* ; def. app. | Π A B ; fun. type e := t ; term | Set ; universe | .p ; field t* := t₁ … tₙ e* := e₁ … eₙ
Figure 2. Syntax of terms in β-normal-form
data Nat where { zero : Nat; suc : Nat → Nat } Γ ⊢ zero ≈ zero : Nat ↦ □ Γ ⊢ suc t ≈ suc u : Nat ↦ (⊤| Γ ⊢ t ≈ u : Nat) Γ, x : ΠAΠBC ⊢ x t u : T ≈ x t’ u’ : T’ ↦ (⊤| Γ, x : ΠABC ⊢ t≈t’ : A) ∧ (⊤| Γ, x : ΠABC ⊢ u:B[t] ≈ u’:B[t’]) Γ, x : ?α ⊢ x t ≈ x t’ : T ↦ (?α| ”) Γ, x : ΠAB, y : ΠAB ⊢ x t ≈ y t ↦ (⊥| ”)
If both heads are are definitions, we do not guess.
plus : Nat → Nat → Nat plus zero n = n plus (suc m) n = suc (plus m n) x y : Nat ⊢ plus x y = plus ?α ?β ↦ (?α| ” ) x y : Nat ⊢ plus x y = plus y x ↦ (⊥| ” )
Binder-headed constraints reduce by expanding the context:
Γ ⊢ λx.t ≈ λx.u : Π(x:A)B ↦ (⊤| Γ, x:A ⊢ t ≈ u : B)
In case of heterogeneous binders, we cannot give variables in the context a single type:
Γ ⊢ λx.t : Π(x:A)B ≈ λx.u :Π(x:A’)B’ : Set ↦ (⊤| Γ, x:⬚ ⊢ t : B ≈ u : B’)
Blocking until Γ ⊢ A≈A’ : Set ↦ □
and
Γ, x:A ⊢ B≈B’ : Set ↦ □
would be too restrictive.
One way of fixing this is introducing a twin-type [Gundry, 2013].
Γ ⊢ λx.t : Π(x:A)B ≈ λx.u :Π(x:A’)B’ : Set ↦ (⊤| Γ, x: A‡A’ ⊢ t : B ≈ u : B’)
Γ ⊢ Π(x:A)B ≈ Π(x:A’)B’ : Set
Notation: ÇÒ ⊢ t ≈ u : B‡B’
where Γ ⊢ t : B
and Γ’ ⊢ t : B
.
We use a simpler presentation than the original
(only twin-types, no twin-variables).
We suspect it is sound.
Eventually we get to a constraint we can actually solve!
𝒞 = ÇÒ ⊢ ?α x₁ … xₙ ≈ t[x₁,…,xₙ] : B’‡B
Two cases:
Γ,B ≈ Γ’,B’ ↦ □
𝒞 ↦ ⊤ ; [?α ≔ λx₁…xₙ.t]
Γ,B ≈ Γ’,B’ ↦ 𝒟₁ ∧ … ∧ 𝒟ₙ
𝒞 ↦ ((𝒟̄₁ ∧ … ∧ 𝒟̄ₙ) ∨ ?α | 𝒞)
This technique shines in examples with a big number of constraints that Agda struggles with.
Implementation | OK | Time | Memory |
---|---|---|---|
Tog-Twins | OK | 455s | 1122MB |
Tog-Twins + HC+M | OK | 101s | 405MB |
Agda | oom | 10998s | 2GB |
Agda + sharing | oom | 10683s | 2GB |
Hash consing + memoization also helps.
Thanks!
We need to check that types are well-behaved wrt. to unification:
Γ₁ ⊢ A type Γ₂ ⊢ B type Γ₁‡Γ₂ ⊢ A : Set ≈ B : Set ↦ ⊤ ──────────────────────────────────── Γ₁ ⊢ B type.
Γ₁ ⊢ A type Γ₁ ⊢ t : A Γ₂ ⊢ B type Γ₁‡Γ₂ ⊢ A : Set ≈ B : Set ↦ □ ──────────────────────────────────── Γ₁ ⊢ t : B
· ⊢ ?α : T Γ₁ ⊢ ?α x₁ … xₙ : A Γ₂ ⊢ t : B FV(t) ⊆ {x₁, …, xₙ} Γ = Γ₁‡Γ₂ Γ ⊢ A ≈ B : Set ↦ □ ∀x ∈ fvs(t), Γ = (Γ’,x:A₁‡A₂,Δ). Γ’ ⊢ A ≈ A’ : Set ↦ □ ───────────────────────────────────── · ⊢ λx₁…xₙ.t : T