a Manifesto

AIM XXX in Munich

**Jesper Cockx**

13 September 2019

_+_ : 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

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

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

\[ \frac{\Gamma \vdash e : x =_A y}{\Gamma \vdash x \equiv y} \]

But when to apply this rule?

Typechecking becomes not just *undecidable*, but also *completely unfeasible* in practice.

Rewrite rules to the rescue!

_+_ : 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)

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

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

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

```
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...
```

- Disallow rewriting of type constructors
- Check
**confluence**of rewrite rules

How? Use the options `--rewriting`

and `--confluence-check`

*

(∗) Only checks *local* confluence so far

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

We could have:

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

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

No.

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)`

?

No.

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

We want equality to be algorithmic *and* extensible.

We want to abstract.

We want to compute.