Intentional equality is fragile

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

  +-comm : (m n : Nat) → m + n ≡ n + m
  +-comm zero    n = {!refl!}
  -- ^ Error: n != n + zero
  +-comm (suc m) n = {!cong suc (+-comm m n)!}
  -- ^ Error: suc _y_69 != n + suc m

Intentional equality is anti-modular

  test₁ : [] ++ xs ≡ xs
  test₁ = refl

  record Monoid (A : Set) : Set where
    field
      mempty : A
      _<>_   : A → A → A
      zero-l : mempty <> y ≡ y

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

    test₂ : mempty <> x ≡ x
    test₂ = {!refl!}
    -- ^ Error: mempty <> x != x of type A

Intentional equality breaks extensibility

  record Except : Set₁ where
    field
      Exception : Set
      raise : {A : Set} → Exception → A
      raise-fun : ∀ e → raise {Π A B} e ≡ λ x → raise {B x} e
      -- ...

  postulate except : Except
  open Except except

  test₃ : raise {Bool → Bool} x ≡ λ b → raise x
  test₃ = {!refl!}
  -- ^ Error: Bool → Bool != Bool

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
    mempty : A
    _<>_   : A → A → A
    zero-l : mempty <> y ≡ y
    zero-r : x <> mempty ≡ 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 <> mempty) <> y) <> (mempty <> z)
          ≡ x <> (y <> z)
  test₂ = {!refl!}

Rewrite rules make type theory extensible

record Except : Set₁ where
  field
    Exception : Set
    raise : {A : Set} → Exception → A
    raise-fun : ∀ e → raise {Π A B} e ≡ λ x → raise {B x} e
    -- ...

postulate except : Except
{-*# REWRITE Except.raise-fun except #-}

Rewrite rules make type theory extensible (2)

record Catch (e : Except) : Set₁ where
  open Except e
  field
    catch : (P : Bool → Set)
        (ptrue : P true) (pfalse : P false)
        (handle : ∀ e → P (raise e))
      → (b : Bool) → P b
    -- ...

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

Why stop at rewrite rules?

We could have:

• Rewrite rules on projections!
• User-defined eta rules!
• User-defined coverings!

We want to compute.

We want to define types that classify computations.

We want to write programs that inhabit those types.

We want types to depend on those programs.

We want programs in types to compute.

We want to abstract.

We want programs to be modular.

We want to build abstractions using types.

We want types to depend on those abstractions.

We want to reason abstractly about abstract programs.

Do we want to choose between abstraction and computation?

Do we want to be anti-modular and anti-extensible, or rely on fragile computation rules?

Choose to be forever doomed to the concrete hell of Bools and Nats, or live on an abstract cloud in the heavens but unable to touch the surface?

Will we let our language limit what we can express?

Are we happy to say that 0 + k is k but not k + 0?

Are we fine with the fact that [] ++ xs is xs but not mempty <> xs?

Should we have p = (fst p , snd p) : A × B, but not xs = x ∷ xs' : Vec A (suc n)?

We want to combine abstraction and computation.

We want our programs to compute how we want, where we want, and when we want.

We want equality to be algorithmic and extensible.