Intentional equality considered harmful

• It is fragile
• It is anti-modular
• It breaks extensibility

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 make computation robust

_+_ : Nat → Nat → Nat
zero    + n = n
(suc m) + n = suc (m + n)

+zero : m +  ≡ m
+zero = ⋯

+suc : m + (suc n) ≡ suc (m + n)
+suc = ⋯

{-# REWRITE +zero +suc #-}

+-comm : (m n : Nat) → m + n ≡ n + m
+-comm zero    n = refl
+-comm (suc m) n = cong suc (+-comm m n)

Rewrite rules make type theory modular

record Monoid (A : Set) : Set where
  field
    ∅      : A
    _·_    : A → A → A
    zero-l : ∅ · y ≡ y
    zero-r : x · ∅ ≡ x
    assoc  : (x · y) · z ≡ x · (y · z)
  {-*# REWRITE zero-l assoc #-}  -- (*) WIP

module _ {A : Set} (m : Monoid A) where
  open Monoid m

  test₂ : ((x · ∅) · y) · (∅ · z) ≡ x · (y · z)
  test₂ = {!refl!}

Rewrite rules make type theory extensible

postulate
  Exception : Set
  raise : {A : Set} → Exception → A
  raise-fun : ∀ e → raise {Π A B} e ≡ λ x → raise {B x} e
{-# REWRITE raise-fun #-}

module _ (P : Bool → Set) (ptrue : P true)
  (pfalse : P false) (handle : ∀ e → P (raise e)) where
  postulate
    catch       : (b : Bool) → P b
    catch-true  :       catch true      ≡ ptrue
    catch-false :       catch false     ≡ pfalse
    catch-raise : ∀ e → catch (raise e) ≡ handle e
{-# REWRITE catch-true catch-false catch-raise #-}

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) 

test : Nat
test = if 0' then  else  -- 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

A practical typechecker for MLTT + rewrite rules

Confluence + no rewriting of type constructors give us the following guarantees:

• Typechecker says yes ⇒ term is type-correct
• Typechecker says no ⇒ term has type error
• Typechecker loops ⇒ rules are non-terminating

MLTT

• Decidable typechecking ☺
• Anti-modular and anti-experimentation ☹

MLTT + equality reflection

• Freedom to reflect arbitrary equalities ☺
• Typechecking requires user input ☹

MLTT + confluent rewrite rules

• Reflect any confluent rewrite system ☺
• Typechecking works in practice ☺

Rewrite rules will soon be your best friend!