## Main challenges

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

TYPES 2023 in Valencia

Jesper Cockx

14 June 2023

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.

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)

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

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

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

We require the following operations on scopes:

- An
**empty scope** - A
**singleton scope** - A
**disjoint union**of scopes - A
**weakening**operation on variables - A
**complement**of each subscope **Decidable equality**of variables

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.

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`

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

If \(α₁ ⋈ α₂ ≡ γ\) and \(β₁ ⋈ β₂ ≡ γ\), then \(γ₁ ⋈ γ₂ ≡ α₁\), \(γ₃ ⋈ γ₄ ≡ α₂\), \(γ₁ ⋈ γ₃ ≡ β₁\), \(γ₂ ⋈ γ₄ ≡ β₂\)

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 ] ⋄ γ

We indexed syntax over scopes to have more precise types, but they should not affect the run-time!

**Problem.** The (size of the) scope is needed at
run-time for constructing injections, so it cannot be erased:

-- Impossible to implement both: inl : {@0 α β : Scope} → α ⊆ (α ⋄ β) inr : {@0 α β : Scope} → β ⊆ (α ⋄ β)

*Can we find a better representation that allows weakening over a
runtime-erased scope?*

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 : α ⋈ β₁ ≡ δ → δ ⋈ β₂ ≡ γ → α ⋈ (β₁ ⋄ β₂) ≡ γ

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*

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!