Dependent Type-Checking with Twin Types

Víctor López Juan

2017-12-13
view source

Created: 2017-12-13 ons 16:16

1 Motivation

There are few descriptions of implementations of Agda-like languages with an emphasis of performance.

We aim to fill this gap.

2 An Agda-like language

  • Universe: Set
  • Dependent functions: (x : A) → B : Set
  • Records:

    record Sigma (A : Set) 
                 (B : A → Set) : Set where
      constructor pair
      field   fst : A 
              snd : B fst
    
  • Induction-recursion
  • Built-in equality with J

2.1 Induction-recursion

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)

2.2 Equality

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

3 Metavariables

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?

3.1 Typechecking in the presence of metavariables

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.

4 A unification problem

Type-checking a program with metavariables
↔ solving its corresponding unification problem
(see [Mazzoli, Abel 2016])

Σ,Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)

  • Σ,Θ is the signature
  • 𝒞ᵢ are constraints
  • ℬᵢ are blockers

4.1 Signature

Σ,Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)

Σ 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.

4.2 Constraints

Σ, Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)

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.

4.3 Blockers

Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)

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

5 Solution to a unification problem

Σ,Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ)

  • A solution to a wf. constraint 𝒞 = Γ ⊢ t:A ≈ u:B is a metasubstitution Θ such that
    (Γ ⊢ t:A ≡ u:B)[Θ].
  • A solution to a unification problem
    Θ; (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ) is a metasubstitution Θ’, such that:
    1. Θ’ is a solution to each 𝒞ᵢ.
    2. Θ’ has no uninstantiated metavariables.
    3. Θ’ is the unique such solution.

5.1 How to find a solution

We i) break the constraints into smaller ones
   ii) until they give us the solution Θ’.

piñata.jpg

Figure 1: Σ,Θ; (ℬ₁| 𝒞₁)∧…∧(ℬₙ| 𝒞ₙ) ⤏* Σ,Θ’; □ cc-by-sa

6 A unification algorithm

We will define a unification relation ().

Θ| 𝒞 ↦ (ℬ₁| 𝒟₁) ∧ … ∧ (ℬₙ| 𝒟ₙ); Θ’

The algorithm () applies () to unblocked constraints.

             Θ| 𝒞ᵢ ↦ (ℬ⃗|𝒟⃗); Θ’ 
────────────────────────────────────────────────
 Θ; …∧ (⊤| 𝒞ᵢ) ∧… ⤏ Θ++Θ’;…∧ (ℬ⃗|𝒟⃗) ∧…

Notation: 𝒞 ↦ (ℬ₁| 𝒞₁) ∧ … ∧ (ℬₙ| 𝒞ₙ).
When n=0, we write 𝒞 ↦ □.

7 Our unification relation

Θ| 𝒞 ↦ (ℬ⃗|𝒟⃗); Θ’, where 𝒞 = Γ ⊢ t:A ≈ u:B

  1. If t≡u are syntactically equal, we are done: 𝒞 ↦ □.
  2. Otherwise, check the heads of the β-WHNF term.
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

7.1 Application or constructor head

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 ↦ (⊥| ”)

7.2 Definition head

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
   ↦ (⊥| ” )

7.3 Heterogeneous binder head, or twin introduction

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.

7.3.1 Introducing twin types

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.

7.4 Instantiating metavariables

Eventually we get to a constraint we can actually solve!

𝒞 =  ÇÒ ⊢ ?α x₁ … xₙ ≈ t[x₁,…,xₙ] : B’‡B

Two cases:

  • if Γ,B ≈ Γ’,B’ ↦ □
    then 𝒞 ↦ ⊤ ; [?α ≔ λx₁…xₙ.t]
  • if Γ,B ≈ Γ’,B’ ↦ 𝒟₁ ∧ … ∧ 𝒟ₙ
    then 𝒞 ↦ ((𝒟̄₁ ∧ … ∧ 𝒟̄ₙ) ∨ ?α | 𝒞)

8 Performance

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.

9 Concluding remarks

  • Many details of higher-order unification are not explained in the presentation (pruning in its many forms, occurs-checking, η-expansion of metavariables and their arguments, etc…).
  • Twin-types and the blocking algebra help avoid ill-typed terms without blocking excessively.
  • Hash-consing speeds things up significantly.

Thanks!

9.1 Conjectures for avoiding twin variables (1/3)

We need to check that types are well-behaved wrt. to unification:

  Γ₁    ⊢ A type 
  Γ₂    ⊢ B type 
  Γ₁‡Γ₂ ⊢ A : Set ≈ B : Set  ↦  ⊤
────────────────────────────────────
  Γ₁    ⊢ B type.

9.2 Conjectures for avoiding twin variables (2/3)

  Γ₁    ⊢ A type        Γ₁ ⊢ t : A
  Γ₂    ⊢ B type
  Γ₁‡Γ₂ ⊢ A : Set ≈ B : Set  ↦  □
────────────────────────────────────
  Γ₁    ⊢ t : B

9.3 Conjectures for avoiding twin variables (3/3)

  · ⊢ ?α : 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