SPLS 2020

**Jesper Cockx**, Nicolas Tabareau, and Théo Winterhalter

21 October 2020

- Formation rules: \(\quad\)
`Bool : Type`

- Introduction rules: \(\quad\)
`true false : Bool`

- Elimination rules:

if`pt : P true`

and`pf : P false`

then`if b then pt else pf : P b`

- Computation rules:

`if true then pt else pf ↝ pt`

- Strict positivity
- Coverage of pattern matching
- Structural recursion

Required to ensure soundness, type preservation, and effective typechecking!

What if this is not enough?

- Option 1: use
`postulate`

- Option 2: hack the language
- Option 3: use a language with
*rewrite rules*

-- 1. Enable rewriting and import primitives: {-# OPTIONS --rewriting #-} open import Agda.Primitive renaming (Set to Type) open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite -- 2. Postulate some things: postulate id : {A : Set} → A → A id-comp : ∀ {A} {x : A} → id x ≡ x -- 3. Register the rewrite rule: {-# REWRITE id-comp #-}

data Vec (A : Set) : Nat → Set where [] : Vec A 0 _∷_ : A → Vec A n → Vec A (suc n)

rev : Vec A n → Vec A n rev xs = rev-acc xs [] where rev-acc : Vec A n → Vec A m → Vec A (m + n) rev-acc [] ys = {! ys !} -- ^ Error: m != m + 0 rev-acc (x ∷ xs) ys = {! rev-acc xs (x ∷ ys)!} -- ^ Error: suc (m + n) != m + (suc n)

+zero : m + 0 ≡ m +zero = ⋯ +suc : m + (suc n) ≡ suc (m + n) +suc = ⋯ {-# REWRITE +zero +suc #-} rev-acc : Vec A n → Vec A m → Vec A (m + n) rev-acc [] ys = ys rev-acc (x ∷ xs) ys = rev-acc xs (x ∷ ys)

postulate S¹ : Type base : S¹ loop : base ≡ base module _ (P : S¹ -> Set) (pbase : P base) (ploop : pbase ≡ pbase [ P ↓ loop ]) where postulate elim-S¹ : (x : S¹) -> P x elim-S¹-base : elim-S¹ base ≡ pbase {-# REWRITE elim-S¹-base #-} postulate elim-S¹-loop : apd elim-S¹ loop ≡ ploop {-# REWRITE elim-S¹-loop #-}

postulate _//_ : (A : Set) (R : A → A → Prop) → Set proj : A → A // R quot : ∀ x y → R x y → proj x ≐ proj y ∈ A // R //-rec : (f : A → B) → (q : ∀ x y → R x y → f x ≐ f y) → (x : A // R) → B //-beta : (f : A → B) → (q : ∀ x y → R x y → f x ≐ f y) → (x : A) → //-rec f q (proj x) ≡ f x {-# REWRITE //-beta #-}

\[ \frac{\Gamma \vdash e : x =_A y}{\Gamma \vdash x \equiv y} \]

But when to apply this rule?

Typechecking becomes not just *undecidable*, but also *completely unfeasible* in practice.

Instead we mark specific equalities as *rewrite rules* that can be applied *automatically*!

Any equality of the form \[ eq : ∀\ x₁\ …\ xₖ → f\ p₁\ …\ pₙ ≡ v \] can be used as a rewrite rule, provided:

- \(p₁ … pₙ\) are
*patterns* - \(p₁ … pₙ\) are
*linear*in \(x₁ … xₖ\) - \(f\ p₁\ …\ pₙ\) and \(v\) have the
*same type* - \(f\ p₁\ …\ pₙ\) does
*not reduce*

Patterns can be *higher order Miller patterns*:

postulate rew₁ : f (λ x → x) ≡ t₂ rew₂ : ∀ (y : T) → f (λ x → y) ≡ y rew₃ : ∀ (q : T → T) → f (λ x → q x) ≡ q t₃ rew₄ : ∀ (y : T) → h (λ (p : T → T) → p y) ≡ y {-# REWRITE rew₁ rew₂ rew₃ rew₄ #-}

Miller fragment: Each pattern variable must be applied to *distinct bound variables*

- Non-linear rewrite rules
- Rewriting modulo \(η\)-equality
- Rewriting modulo irrelevance
- Rewriting in parametrized modules
- Rewriting universe-polymorphic functions
- Rewriting in presence of metavariables

- … logical soundness?
- … decidable typechecking?
- … type preservation?

A rewrite rule `0 ↝ 1`

breaks soundness!

… but that’s no different from using `postulate`

.

**Theorem.** If all rewrite rules are provable, then soundness is preserved.

*Proof.* By translation to extensional type theory.

A rewrite rule `loop ↝ loop`

breaks termination!

… but termination is not a critical property.

**Theorem.** When the usual conversion algorithm terminates, its answer is still correct.

*Proof.* Computing the weak-head normal form preserves definitional equality.

A rewrite rule `true ↝ 42`

breaks subject reduction…

and this is actually a serious problem!

We can limit rewriting to homogeneous rules, but is that enough?

```
postulate rew : Nat → Nat ≡ Nat → Bool
{-# REWRITE rew #-}
0' : Bool
0' = (λ (x : Nat) → x) 0
test : Nat
test = if 0' then 42 else 9000 -- Uh oh...
```

```
record Box (A : Set) : Set where
constructor box
field unbox : A
open Box
postulate rew : Box (Nat → Nat) ≡ Box (Nat → Bool)
{-# REWRITE rew #-}
0' : Bool
0' = unbox {Nat → Bool} (box {Nat → Nat} id) 0
test : Nat
test = if 0' then 42 else 9000 -- Uh oh...
```

```
postulate
X : Set
rew₁ : X ≡ Nat → Nat
rew₂ : X ≡ Nat → Bool
{-# REWRITE rew₁ rew₂ #-}
test : Nat
test = if 0' then 42 else 9000 -- Uh oh...
```

Again we have `Nat → Nat == Nat → Bool`

!

- Rewrite rules should preserve typing
- No rewriting of type constructors
- Rewrite rules + β-reduction should be
*confluent*

Two problems:

- Checking local confluence is not enough
- Checking termination first is not possible

⇒ standard criterion on critical pairs fails!

We need a stronger property: the *triangle property* of parallel reduction as used by Tait and Martin-Löf

Parallel reduction \(⇛\) reduces all redexes in one step:

\[↝ \ ⊆\ ⇛\ ⊆\ ↝^*\]

**Triangle property:** each \(t\) has a *best reduct* \(ρ(t)\)

The `--confluence-check`

flag in Agda:

- 2.6.1:
*local*confluence using critical pairs - 2.6.2:
*global*confluence using triangle property

Two categories of use cases for rewrite rules:

- Make more terms typecheck by turning propositional equalities into definitional ones
- Define new primitives that go beyond standard MLTT and make them compute

The triangle property can ensure rewrite rules preserve subject reduction!

- Agda documentation:

agda.readthedocs.io - TYPES paper on rewriting in Agda:

https://doi.org/10.4230/LIPIcs.TYPES.2019.2 - POPL paper on safety of rewrite rules:

https://hal.archives-ouvertes.fr/hal-02901011 - Formalization in MetaCoq:

https://github.com/TheoWinterhalter/template-coq/

What do you want to hear more about:

- More examples?
- More details on RTT and its formalization?
- More detail of implementation of rewrite rules and confluence check?