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

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