SPLS 2020

21 October 2020

Introduction

Extending Martin-Löf Type Theory

• 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

Restrictions imposed by proof assistants

• Strict positivity
• Coverage of pattern matching
• Structural recursion

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

Drawing outside the lines

What if this is not enough?

• Option 1: use postulate
• Option 2: hack the language
• Option 3: use a language with rewrite rules

Rewrite rules in Agda

Using rewrite rules in three simple steps

-- 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 #-}


Definitional equality is fragile

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)


Rewrite rules to the rescue!

+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)


HITs that compute

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 #-}


Defining quotient types

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 #-}


Extending type theory with rewrite rules

The sledgehammer of equality reflection

$\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!

Rewrite rules, in general

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

Higher-order patterns

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

Other extensions of rewriting

• Non-linear rewrite rules
• Rewriting modulo $η$-equality
• Rewriting modulo irrelevance
• Rewriting in parametrized modules
• Rewriting universe-polymorphic functions
• Rewriting in presence of metavariables

Rewrite rules are great! But what about…

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

Logical soundness

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.

Termination

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.

Type preservation

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?

Breaking type safety by rewriting function types

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

Breaking type safety by rewriting type constructors

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

Breaking type safety with non-confluence

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!

Three requirements to ensure subject reduction:

1. Rewrite rules should preserve typing
2. No rewriting of type constructors
3. Rewrite rules + β-reduction should be confluent

Checking confluence

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

Parallel reduction $⇛$ reduces all redexes in one step:

$↝ \ ⊆\ ⇛\ ⊆\ ↝^*$

The triangle property

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

Checking confluence with the triangle property:

The --confluence-check flag in Agda:

• 2.6.1: local confluence using critical pairs
• 2.6.2: global confluence using triangle property

Conclusion

Rewrite rules are great!

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!