# Abstraction and Computation: a Manifesto

AIM XXX in Munich

13 September 2019

# Intentional equality considered harmful

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

But when to apply this rule?

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

## Should definitional equality be extensible or algorithmic?

Rewrite rules to the rescue!

# Rewrite rules to the rescue

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


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

(∗) Only checks local confluence so far

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

# Manifesto

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

No.

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

No.

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

We want to abstract.

We want to compute.