Problem: Agda has bugs

Agda is ~100 KLOC of Haskell, not all of it is correct. [citation needed]

Since 2007, there have been 65 bugs that broke consistency in some way.

Many of them come from (interactions between) experimental features, but this is still not ideal.

Solution: Agda Core

We want:

• A small core language for Agda
• A formal definition of its typing rules
• A correct-by-construction type checker

This is the goal of my ongoing Agda Core project (funded by NWO Veni)

Main challenges

• Deciding on the right feature-set for Agda Core
• Formalizing syntax with binders
• Ensuring totality

Why scope your syntax?

Formalizing and/or implementing a dependently typed language can be hard.

We can offload the boring complexity onto the type checker so we can focus on the essential complexity.

Hence, well-scoped syntax.

Well-scoped de Bruijn

  data Var : (n : Nat) → Set where
    zero :         Var (suc n)
    suc  : Var n → Var (suc n)

  data Term (n : Nat) : Set where
    var : Var n           → Term n
    lam : Term (suc n)    → Term n
    app : Term n → Term n → Term n

Limitations:

• Hard to understand for humans
• Permutations of variables are invisible in the type
• Forces linear lookup on contexts and environments

An abstract scope interface

We require the following operations on scopes:

1. An empty scope
2. A singleton scope
3. A disjoint union of scopes
4. A weakening operation on variables
5. A complement of each subscope
6. Decidable equality of variables

Why do we need complements?

The typing rule for case expressions in Agda Core:

\[ \frac{\begin{array}{c} \Gamma = \Gamma_1(x : A)\Gamma_2 \qquad A \leadsto \texttt{D}~\overline{p} \\ \forall (c : (\overline{y} : \Delta) → D~\overline{v}).~\Gamma_1(\overline{y} : \Delta)\Gamma_2\sigma \vdash b : B\sigma \\ (\text{where } \sigma = [x ↦ c~\overline{y}]) \end{array} }{ \Gamma \vdash \texttt{case}~x~\texttt{of}~\overline{c~\overline{y} \mapsto b} : B } \]

This requires the ability to delete a variable from a scope, which is a kind of complement.

Proof-relevant separation algebra

We work with a ternary relation that indicates how a scope can be split in two disjoint parts:

\[ p : α ⋈ β ≡ γ \]

We can then define elementhood and complement:

• α ⊆ β = Σ Scope (λ γ → α ⋈ γ ≡ β)
• x ∈ α = [ x ] ⊆ α
• p ᶜ = fst

One more missing operation

To define substitution for case expressions, we need a four-way separation:

Scopes as lists of names

Why not simply represent scopes as lists of names?

  Scope  = List Name
  ∅      = []
  [ x ]  = x ∷ []
  _⋄_    = _++_

  data _⋈_≡_ : Scope → Scope → Scope → Set where
    done  :                     ∅ ⋈         ∅ ≡         ∅
    left  : α ⋈ β ≡ γ → [ x ] ⋄ α ⋈         β ≡ [ x ] ⋄ γ
    right : α ⋈ β ≡ γ →         α ⋈ [ x ] ⋄ β ≡ [ x ] ⋄ γ

Problem. The (size of the) scope is needed at run-time for weakening!

A fancy type of separations

We can avoid representing scopes at run-time by adding constructors to the separation type:

  data _⋈_≡_ : (α β γ : Scope) → Set where
    ∅-l  : ∅         ⋈ β         ≡ β
    ∅-r  : α         ⋈ ∅         ≡ α
    join : α         ⋈ β         ≡ (α ⋄ β)
    swap : α         ⋈ β         ≡ (β ⋄ α)
    ⋄-ll :       α₂  ⋈ β         ≡ δ       → α₁ ⋈ δ  ≡ γ
         → (α₁ ⋄ α₂) ⋈ β         ≡ γ
    ⋄-lr :  α₁       ⋈ β         ≡ δ       → δ  ⋈ α₂ ≡ γ
         → (α₁ ⋄ α₂) ⋈ β         ≡ γ
    ⋄-rl : α         ⋈       β₂  ≡ δ       → β₁ ⋈ δ  ≡ γ
         → α         ⋈ (β₁ ⋄ β₂) ≡ γ
    ⋄-rr : α         ⋈  β₁       ≡ δ       → δ  ⋈ β₂ ≡ γ
         → α         ⋈ (β₁ ⋄ β₂) ≡ γ

Problem with this approach

Now scopes are not needed at run-time, but separation proofs are no longer unique:

  enlarge : (α₁ ⋄ α₂) ⋈ β ≡ γ → (α₁ ⋄ α₂) ⋈ β ≡ γ
  enlarge p = ⋄-ll join (⋄-rr join p)

This causes problems with the termination checker.

Because of this, constructing four-way separation still seems to be impossible without inspecting the scopes.

¯\_(ツ)_/¯

Lesson 1. Proof-relevant separation algebras are a useful interface for working with well-scoped syntax.

Lesson 2. (Conjecture) It is impossible to implement this interface such that both:

• scopes are run-time irrelevant
• separation proofs are unique

A word of caution

Expressive type systems such as QTT can be a powerful tool for designing an API.

However, it’s easy to end up with a design that has no reasonable implementation.

Keep yourself honest and always develop at least one implementation alongside your API!

Questions?