Type checking relies on computation

append : Vec A m → Vec A n → Vec A (m + n)
append []       ys = ys
  -- ^ 0       + n = n
append (x ∷ xs) ys = x ∷ (append xs ys)
  -- ^ (suc m) + n = suc (m + n)

Computation is fragile

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

Computation breaks abstraction

postulate
  M      : Set
  ∅      : M
  _<>_   : M → M → M
  zero-l : ∅ <> y ≡ y
  zero-r : x <> ∅ ≡ x
  assoc  : (x <> y) <> z ≡ x <> (y <> z)

test : ((x <> ∅) <> y) <> (∅ <> z) ≡ x <> (y <> z)
test = {! refl !}

Abstract types like M are harder to work with than concrete types like List!

Rewrite rules to the rescue!

{-# REWRITE zero-l zero-r assoc #-}

test' : ((x <> ∅) <> y) <> (∅ <> z) ≡ x <> (y <> z)
test' = refl

Computation breaks extensibility

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

But //-rec does not compute!

Rewrite rules to the rescue!

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

The sledgehammer of equality reflection

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

Should definitional equality be extensible or algorithmic?

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

How safe are rewrite rules?

Answer: not very

Breaking type safety in 3.. 2.. 1..

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

Tame your rewrite rules in two easy steps!

1. Disallow rewriting of type constructors
2. Check confluence of rewrite rules

A non-confluent example

postulate
  max : Nat → Nat → Nat
  max-diag  : max m m ≡ m
  max-assoc : max (max k l) m ≡ max k (max l m)

{-# REWRITE max-diag max-assoc #-}

-- ———— Errors ————————————————————————————————————————
-- Confluence check failed: max (max k l) (max k l)
-- reduces to both max k (max l (max k l)) and max k l
-- which are not equal because max l (max k l) != l of
-- type Nat
--
-- Confluence check failed: max (max k k) m reduces to
-- both max k (max k m) and max k m which are not equal
-- because max k m != m of type Nat

Unchaining the power of computation

With the power of rewrite rules, you can:

• make more terms typecheck without annotations
• extend type theory with new constructions