Operations on Syntax Should Not Inspect Their Scope (…Or Should They?)

TYPES 2023 in Valencia

Jesper Cockx

14 June 2023


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

Well-scoped syntax

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


  • 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:

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

Towards a concrete implementation

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

To erase or not to erase?

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?

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!