# How to tame your rewrite rules

TYPES ’19 in Oslo

14 June 2019

## Trigger warning

This talk may contain:

• violations of type safety
• fire-breathing dragons

# Computation: We Are Doing It Wrong

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

But when to apply this rule?

## Should definitional equality be extensible or algorithmic?

Rewrite rules to the rescue!

# Rewrite rules in action

## Rewrite rules make computation robust

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

+zero : m + 0 ≡ 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 #-}


# Taming your rewrite rules

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

How? Use the options --rewriting and --confluence-check*

(*) Now available in Agda, soon also in Coq!

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


# Conclusion

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

With termination we regain decidable typechecking

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 ☺