Posted by Jesper on October 21, 2019

This is the first in a series of three blog posts on rewrite rules in Agda. In contrast to my previous post, this post will decidedly *non-introductory*. Instead, we will have some fun by doing unsafe things and hacking things into the core reduction machinery of Agda.

The main part of this post will consist of several examples of how to use rewrite rules to go beyond the usual boundaries set by Agda and define your *own* computation rules. The next two posts in this series will go more into how rewrite rules work in general and the metatheory of type theory extended with rewrite rules.

## Why rewrite rules?

The way I learned type theory from Simon Thompson’s book, each type former is defined by four sets of rules:

The

**formation rule**(e.g.`Bool : Set`

)The

**introduction rules**(e.g.`true : Bool`

and`false : Bool`

)The

**elimination rules**(e.g. if`P : Bool → Set`

,`b : Bool`

,`pt : P true`

, and`pf : P false`

, then`if b then pt else pf : P b`

)The

**computation rules**(e.g.`if true then pt else pf = pt`

and`if false then pt else pf = pf`

)

Most of the time when we work in Agda, we don’t introduce new types by directly giving these rules. That would be very unsafe, as there’s no easy way for Agda to check that the given rules make sense. Instead, we can introduce new rules through *schemes* that are well-known to be safe, such as strictly positive datatypes and terminating functions by dependent pattern matching.

However, if you’re experimenting with adding new features to dependently typed languages or if you’re a heavy user of them, you might find working within these schemes a bit too restrictive. You might be tempted to use `postulate`

to define new types and terms, or to turn off the safety checks for termination, positivity, and/or universe consistency. Yet there is one thing that cannot be simply added by using these tricks. This is exactly the one thing that breathes life into the type theory: the computation rules. This is the purpose of *rewrite rules* in Agda (as well as in some other languages like Dedukti): to allow the user of the language to extend the language’s notion of definitional equality with additional computation rules.

Concretely, given a proof (or a postulate) `p : ∀ x₁ ... xₙ → f u₁ ... uₙ ≡ v`

, you can register it as a rewrite rule with a pragma `{-# REWRITE p #-}`

. From this point on, Agda will automatically reduce instances of the left-hand side `f u₁ ... uₙ`

(i.e. for specific values of `x₁ ... xₙ`

) to the corresponding instance of `v`

. To give a silly example, if `f : A → A`

and `p : ∀ x → f x ≡ x`

, then the rewrite rule will replace any application `f u`

with `u`

, effectively turning `f`

into the identity function `λ x → x`

.

There are some restrictions on what kind of equality proofs can be turned into rewrite rules, which I will go into more detail in the next post. Until then, I hope the examples in this post give a good idea of the kind of things that are possible.

One thing that is perhaps obvious but I want to stress nevertheless is that by design rewrite rules are a *very unsafe* feature of Agda. Compared to using `postulate`

, rewrite rules don’t allow you to break soundness (at least not directly), but they can break core assumptions of Agda such as confluence of reduction and even type preservation. So each time you use a rewrite rule, make sure you know it is justified, or be prepared to suffer the consequences.

With the introduction out of the way, let’s jump into some examples of cool things you can do with rewrite rules.

## Preliminaries

This whole post is written as a literate Agda file. As always, we some basic options and imports. For the purpose of this post, the two most important ones are the `--rewriting`

flag and the import of `Agda.Builtin.Equality.Rewrite`

, which are both required to make rewrite rules work. Meanwhile, the `--prop`

flag enables Agda’s `Prop`

universe (new in Agda 2.6.0), which we will use in some of the examples.

{-# OPTIONS --rewriting --prop #-} open import Agda.Primitive open import Agda.Builtin.Bool open import Agda.Builtin.Nat open import Agda.Builtin.List open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite

As in the previous post, I will make heavy use of generalizable variables to make the code more readable. (Honestly, I’m not sure how I ever managed to write Agda code without them.)

variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level A B C : Set ℓ P Q : A → Set ℓ x y z : A f g h : (x : A) → P x b b₁ b₂ b₃ : Bool k l m n : Nat xs ys zs : List A

To avoid reliance on external libraries, we also need these two basic equality reasoning principles.

cong : (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl transport : (P : A → Set ℓ) → x ≡ y → P x → P y transport P refl p = p

## Example 1: Overlapping pattern matching

To start, let’s look at an example where rewrite rules can solve a problem that is encountered by almost every newcomer to Agda. This problem usually pops up as the question why `0 + m`

computes to `m`

, but `m + 0`

does not (and similarly, `(suc m) + n`

computes to `suc (m + n)`

but `m + (suc n)`

does not). This problem manifests for example when trying to prove commutativity of `_+_`

(the lack of highlighting means the code does not typecheck):

```
+comm : m + n ≡ n + m
+comm {m = zero} = refl
+comm {m = suc m} = cong suc (+comm {m = m})
```

Here, Agda complains that `n != n + zero of type Nat`

. The usual way to solve this problem is by proving the equations `m + 0 ≡ m`

and `m + (suc n) ≡ suc (m + n)`

and using an explicit `rewrite`

statement in the main proof (N.B.: Agda’s `rewrite`

keyword should not be confused with rewrite rules, which are added by a `REWRITE`

pragma. Confusing, I know.)

This problem is something that has both frustrated and fascinated me from the very beginning I started working on type theory. During my master thesis, I worked on adding *overlapping computation rules* to make this problem go away *without* adding any explicit `rewrite`

statements to the proof above.

By using rewrite rules, we can simulate the solution from our paper. First, we need to prove that the equations we want hold as *propositional equalities*:

zero+ : zero + n ≡ n zero+ = refl suc+ : (suc m) + n ≡ suc (m + n) suc+ = refl +zero : m + zero ≡ m +zero {m = zero} = refl +zero {m = suc m} = cong suc +zero +suc : m + (suc n) ≡ suc (m + n) +suc {m = zero} = refl +suc {m = suc m} = cong suc +suc

We mark the equalities that are not already definitional as rewrite rules with a `REWRITE`

pragma:

{-# REWRITE +zero +suc #-}

Now the proof of commutativity works exactly as we wrote before:

+comm : m + n ≡ n + m +comm {m = zero} = refl +comm {m = suc m} = cong suc (+comm {m = m})

Note that there is **no** way to make this proof go through without rewrite rules: it is essential that `_+_`

computes both on its first and second arguments, but there’s no way to define `_+_`

in such a way using Agda’s regular pattern matching.

## Example 2: New equations for neutral terms

The idea of extending existing functions with new computation rules has been taken much further in a very nice paper by Guillaume Allais, Conor McBride, and Pierre Boutillier titled New Equations for Neutral Terms. In this paper, they add new computation rules to classic functions on lists such as `map`

, `_++_`

, and `fold`

. In Agda, we can prove these rules and then add them as rewrite rules (here I only show a subset of the rules in the paper):

map : (A → B) → List A → List B map f [] = [] map f (x ∷ xs) = (f x) ∷ (map f xs) infixr 5 _++_ _++_ : List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) map-id : map (λ x → x) xs ≡ xs map-id {xs = []} = refl map-id {xs = x ∷ xs} = cong (_∷_ x) map-id map-fuse : map f (map g xs) ≡ map (λ x → f (g x)) xs map-fuse {xs = []} = refl map-fuse {xs = x ∷ xs} = cong (_∷_ _) map-fuse map-++ : map f (xs ++ ys) ≡ (map f xs) ++ (map f ys) map-++ {xs = []} = refl map-++ {xs = x ∷ xs} = cong (_∷_ _) (map-++ {xs = xs}) {-# REWRITE map-id map-fuse map-++ #-}

These rules look reasonably simple, but when used together they can be quite powerful. For example, below we show that the expression `map swap (map swap xs ++ map swap ys)`

reduces directly to `xs ++ ys`

, without doing any induction on the lists!

record _×_ (A B : Set) : Set where constructor _,_ field fst : A snd : B open _×_ swap : A × B → B × A swap (x , y) = y , x test₁ : map swap (map swap xs ++ map swap ys) ≡ xs ++ ys test₁ = refl

To compute the left-hand side of the equation to the right-hand side, Agda makes use of `map-++`

(`step₁`

), `map-fuse`

(`step₂`

), built-in eta-equality (`step₃`

), the definition of `swap`

(`step₄`

), and finally the `map-id`

rewrite rule (`step₅`

).

-- Using map-++: step₁ : map swap (map swap xs ++ map swap ys) ≡ map swap (map swap xs) ++ map swap (map swap ys) step₁ = refl -- Using map-fuse (likewise for ys) step₂ : map swap (map swap xs) ≡ map (λ x → swap (swap x)) xs step₂ = refl -- Using eta-expansion step₃ : map (λ x → swap (swap x)) xs ≡ map (λ x → swap (swap (fst x , snd x))) xs step₃ = refl -- Using definition of swap (2x) step₄ : map (λ x → swap (swap (fst x , snd x))) xs ≡ map (λ x → (fst x , snd x)) xs step₄ = refl -- Using map-id (together with eta-contraction) step₅ : map (λ x → (fst x , snd x)) xs ≡ xs step₅ = refl

## Example 3: Higher inductive types

The original motivation for adding rewrite rules to Agda had little to do with overlapping computation rules as in the previous examples. Instead, its purpose was to experiment with defining *higher inductive types*. In particular, it was meant as an alternative for people using clever (but horrible) hacks to make their higher inductive types compute.

A higher inductive type is like a regular inductive type `D`

with some additional *path constructors*, which construct an element of the identity type `a ≡ b`

where `a : D`

and `b : D`

. A classic example is the `Circle`

type, which has one regular constructor `base`

and one path constructor `loop`

:

postulate Circle : Set base : Circle loop : base ≡ base postulate Circle-elim : (P : Circle → Set ℓ) → (base* : P base) → (loop* : transport P loop base* ≡ base*) → (x : Circle) → P x elim-base : ∀ (P : Circle → Set ℓ) base* loop* → Circle-elim P base* loop* base ≡ base* {-# REWRITE elim-base #-}

To specify the computation rule for `Circle-elim`

applied to `loop`

, we need the dependent version of `cong`

, which is called `apd`

in the book.

apd : (f : (x : A) → P x) (p : x ≡ y) → transport P p (f x) ≡ f y apd f refl = refl postulate elim-loop : ∀ (P : Circle → Set ℓ) base* loop* → apd (Circle-elim P base* loop*) loop ≡ loop* {-# REWRITE elim-loop #-}

Interestingly, the type of `elim-loop`

is not even well-formed unless we alreay have `elim-base`

as a rewrite rule! So without rewrite rules, it is even difficult to *state* the computation rule of `Circle-elim`

for `loop`

.

## Example 4: Quotient types

One of the well-known weak spots of intentional type theory is the poor handling of quotient types. One of the more promising attempts at adding quotients to Agda is by Guillaume Brunerie in the initiality project, which uses a combination of rewrite rules and Agda’s new (strict) `Prop`

universe.

Before I can give the definition of the quotient type, we first need to define the `Prop`

-valued equality type `_≐_`

. We also define its corresponding notion of `transport`

, which has to be postulated due to current limitations in the implementation of `Prop`

. Luckily, we can actually make `transportR`

compute in the expected way by postulating the expected computational behaviour and turning it into a rewrite rule.

data _≐_ {A : Set ℓ} (x : A) : A → Prop ℓ where refl : x ≐ x postulate transportR : (P : A → Set ℓ) → x ≐ y → P x → P y transportR-refl : transportR P refl x ≡ x {-# REWRITE transportR-refl #-}

Now we can define the quotient type `_//_`

. Specifically, given a type `A`

and a `Prop`

-valued relation `R : A → A → Prop`

, we construct the type `A // R`

consisting of elements `proj x`

where `x : A`

and `proj x ≡ proj y`

if and only if `R x y`

.

variable R : A → A → Prop postulate _//_ : (A : Set ℓ) (R : A → A → Prop) → Set ℓ proj : A → A // R quot : R x y → proj {R = R} x ≐ proj {R = R} y

The crucial element here is the elimination principle `//-elim`

, which allows us to define functions that *extract* an element of `A`

from a given element of `A // R`

, as long as we have a *proof* `quot*`

that the function behaves the same on `proj x`

and `proj y`

whenever `R x y`

holds. The computation rule `//-beta`

turns this definition of quotients into more than just a static blob of postulates by allowing `//-elim`

to compute when it is applied to a `proj x`

.

//-elim : (P : A // R → Set ℓ) → (proj* : (x : A) → P (proj x)) → (quot* : {x y : A} (r : R x y) → transportR P (quot r) (proj* x) ≐ proj* y) → (x : A // R) → P x //-beta : {R : A → A → Prop} (P : A // R → Set ℓ) → (proj* : (x : A) → P (proj x)) → (quot* : {x y : A} (r : R x y) → transportR P (quot r) (proj* x) ≐ proj* y) → {u : A} → //-elim P proj* quot* (proj u) ≡ proj* u -- Note: The type of //-beta mysteriously does not -- check when I leave out the {R : A → A → Prop}, -- I'm not sure what's up with that. {-# REWRITE //-beta #-}

(As a side note, here is an interesting recent discussion on quotient types in Lean, Coq, and Agda.)

## Example 5: Exceptional type theory

I have a secret to share with you: my first programming language was Java. While I don’t miss most parts of it, sometimes I just long to use a good unchecked exception in my pristine purely functional language. Luckily, my friends over at Inria in Nantes have written the aptly named paper Failure is Not an Option: An Exceptional Type Theory, which shows how to add exceptions to Coq. Through the exceptional power of rewrite rules, we can also encode their system in Agda.

First, we postulate a type `Exc`

with any kinds of exceptions we might want to use (here we just have `runtimeException`

for simplicity). We then add the possibility to `raise`

an exception, producing an element of an arbitrary type `A`

.

postulate Exc : Set runtimeException : Exc raise : Exc → A

By adding the appropriate rewrite rules for each type former, we can ensure that exceptions are *propagated* to the top-level. Below, I give two examples. For positive types such as `Nat`

, exceptions are propagated *outwards*, while for negative types such as function types, exceptions are propagated *inwards*.

raise-suc : {e : Exc} → suc (raise e) ≡ raise e raise-fun : {e : Exc} → raise {A = (x : A) → P x} e ≡ λ x → raise {A = P x} e {-# REWRITE raise-suc raise-fun #-}

To complete the system, we can then add the ability to `catch`

exceptions at specific types. This takes the shape of an eliminator with one additional method for handling the case where the element under scrutiny is of the form `raise e`

.

postulate catch-Bool : (P : Bool → Set ℓ) (pt : P true) (pf : P false) (h : ∀ e → P (raise e)) → (b : Bool) → P b catch-true : ∀ (P : Bool → Set ℓ) pt pf h → catch-Bool P pt pf h true ≡ pt catch-false : ∀ (P : Bool → Set ℓ) pt pf h → catch-Bool P pt pf h false ≡ pf catch-exc : ∀ (P : Bool → Set ℓ) pt pf h e → catch-Bool P pt pf h (raise e) ≡ h e {-# REWRITE catch-true catch-false catch-exc #-}

In their paper, Pierre-Marie and Nicolas show how to build a *safe* version of exceptions on top of this system, using *parametricity* to enforce that all exceptions are caught locally. Please go read their paper if you want to know more!

## Example 6: Observational equality

We can go even further in extending our type theory with new concepts using rewrite rules. For example, we can define *type constructors* that compute according to the type they are applied to. This is the core concept of *observational type theory* (OTT). OTT extends type theory with an observational equality type (here called `_≅_`

) that computes acoording to the type of the elements being compared. For example, an equality proof of type `(a , b) ≅ (c , d)`

**is** a pair of proofs, one of type `a ≅ c`

and one of type `b ≅ d`

.

OTT had a strong influence on the recent development of cubical type theory, which extends it with a *proof-relevant* notion of equality. Yet there are still some things that are possible in OTT but not in cubical, so we should not write it off yet. For example, OTT has *definitional proof irrelevance*, while it is not clear yet how this can be integrated into cubical (although XTT looks very promising).

Below, I define a small fragment of OTT by using rewrite rules in Agda. Since OTT has a proof-irrelevant equality type, I use Agda’s `Prop`

to get the same effect.

First, we need some basic types in `Prop`

:

record ⊤ {ℓ} : Prop ℓ where constructor tt data ⊥ {ℓ} : Prop ℓ where record _∧_ (X : Prop ℓ₁) (Y : Prop ℓ₂) : Prop (ℓ₁ ⊔ ℓ₂) where constructor _,_ field fst : X snd : Y open _∧_

The central type is observational equality `_≅_`

, which should compute according to the types of the elements being compared. Here I give the computation rules for `Bool`

and for function types:

infix 6 _≅_ -- Observational equality postulate _≅_ : {A : Set ℓ₁} {B : Set ℓ₂} → A → B → Prop (ℓ₁ ⊔ ℓ₂) HEq = _≅_ syntax HEq {A = A} {B = B} x y = x ∈ A ≅ y ∈ B postulate refl-Bool : (Bool ≅ Bool) ≡ ⊤ refl-true : (true ≅ true) ≡ ⊤ refl-false : (false ≅ false) ≡ ⊤ conflict-tf : (true ≅ false) ≡ ⊥ conflict-ft : (false ≅ true) ≡ ⊥ {-# REWRITE refl-Bool refl-true refl-false conflict-tf conflict-ft #-} postulate cong-Π : ((x : A) → P x) ≅ ((y : B) → Q y) ≡ (B ≅ A) ∧ ((x : A)(y : B) → y ≅ x → P x ≅ Q y) cong-λ : {A : Set ℓ₁} {B : Set ℓ₂} → {P : A → Set ℓ₃} {Q : B → Set ℓ₄} → (f : (x : A) → P x) (g : (y : B) → Q y) → ((λ x → f x) ≅ (λ y → g y)) ≡ ((x : A) (y : B) (x≅y : x ≅ y) → f x ≅ g y) {-# REWRITE cong-Π cong-λ #-}

To be able to actually reason about equality, OTT also has two more notions: **coercion** and **cohesion**. Coercion allows us to cast an element from one type to the other when we know both types are equal, and cohesion allows us to prove that coercion is computationally a no-op.

infix 10 _[_⟩ _||_ postulate _[_⟩ : A → A ≅ B → B -- Coercion _||_ : (x : A) (Q : A ≅ B) → x ∈ A ≅ x [ Q ⟩ ∈ B -- Coherence

Again, we need more rewrite rules to make sure coercion computes in the right way when applied to specific type constructors. Note that we *don’t* need rewrite rules for coherence, since the result is of type `_ ≅ _`

which is a `Prop`

, so it anyway has no computational content.

Coercing an element from `Bool`

to `Bool`

is easy.

postulate coerce-Bool : (Bool≅Bool : Bool ≅ Bool) → b [ Bool≅Bool ⟩ ≡ b {-# REWRITE coerce-Bool #-}

To coerce a function from `(x : A) → P x`

to `(y : B) → Q y`

we need to:

- Coerce the input from
`y : B`

to`x : A`

- Apply the function to get an element of type
`P x`

- Coerce the output back to an element of
`Q y`

In the last step, we need to use coherence to show that `x`

and `y`

are (heterogeneously) equal.

postulate coerce-Π : {A : Set ℓ₁} {B : Set ℓ₂} → {P : A → Set ℓ₃} {Q : B → Set ℓ₄} → {f : (x : A) → P x} → (ΠAP≅ΠBQ : ((x : A) → P x) ≅ ((y : B) → Q y)) → _≡_ {A = (y : B) → Q y} (f [ ΠAP≅ΠBQ ⟩) λ (y : B) → let B≅A : B ≅ A B≅A = fst ΠAP≅ΠBQ x : A x = y [ B≅A ⟩ Px≅Qy : P x ≅ Q y Px≅Qy = snd ΠAP≅ΠBQ x y (_||_ {B = A} y B≅A) in f x [ Px≅Qy ⟩ {-# REWRITE coerce-Π #-}

Of course this is just a fragment of the whole system, but implementing all of OTT would go beyond the scope of this blog post. Hopefully this at least gives an idea how one could implement the full system.

## Conclusion

With all these examples, I think this blog post has become long enough. If you read all the way to here, I hope you found at least one example that gave you the itch to try rewrite rules yourself. Be sure to let me know if you come up with other cool examples! And if you got interested in the exact workings of rewrite rules in Agda and how they are implemented, stay tuned for the next post in this series.