# Type Theory Unchained

PLNL 2019 in Nijmegen

12 December 2019

## Dependent types: types depend on values

data Vec (A : Set) : Nat → Set where
[]  : Vec A 0
_∷_ : A → Vec A n → Vec A (suc n)

my-vector : Vec Nat 3
my-vector = 1 ∷ 2 ∷ 3 ∷ []


# Rewrite rules in action

## Type checking relies on computation

append : Vec A m → Vec A n → Vec A (m + n)
append []       ys = ys
-- ^ 0       + n = n
append (x ∷ xs) ys = x ∷ (append xs ys)
-- ^ (suc m) + n = suc (m + n)


## Computation is fragile

  rev : Vec A n → Vec A n
rev xs = rev-acc xs []
where
rev-acc : Vec A n → Vec A m → Vec A (m + n)
rev-acc []       ys = {! ys !}
-- ^ Error: m != m + 0
rev-acc (x ∷ xs) ys = {! rev-acc xs (x ∷ ys)!}
-- ^ Error: suc (m + n) != m + (suc n)


## Rewrite rules to the rescue!

+zero : m + 0 ≡ m
+zero = ⋯

+suc : m + (suc n) ≡ suc (m + n)
+suc = ⋯

{-# REWRITE +zero +suc #-}

rev-acc : Vec A n → Vec A m → Vec A (m + n)
rev-acc []       ys = ys
rev-acc (x ∷ xs) ys = rev-acc xs (x ∷ ys)


## Computation breaks abstraction

postulate
M      : Set
∅      : M
_<>_   : M → M → M
zero-l : ∅ <> y ≡ y
zero-r : x <> ∅ ≡ x
assoc  : (x <> y) <> z ≡ x <> (y <> z)

test : ((x <> ∅) <> y) <> (∅ <> z) ≡ x <> (y <> z)
test = {! refl !}


Abstract types like M are harder to work with than concrete types like List!

## Rewrite rules to the rescue!

{-# REWRITE zero-l zero-r assoc #-}

test' : ((x <> ∅) <> y) <> (∅ <> z) ≡ x <> (y <> z)
test' = refl


## Computation breaks extensibility

postulate
_//_    : (A : Set) (R : A → A → Prop) → Set
proj    : A → A // R
quot    : ∀ x y → R x y → proj x ≐ proj y ∈ A // R

//-rec  : (f : A → B)
→ (q : ∀ x y → R x y → f x ≐ f y)
→ (x : A // R) → B


But //-rec does not compute!

## Rewrite rules to the rescue!

postulate
//-beta : (f : A → B)
→ (q : ∀ x y → R x y → f x ≐ f y)
→ (x : A) → //-rec f q (proj x) ≡ f x
{-# REWRITE //-beta #-}


# Extending type theory with rewrite rules

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

## Rewrite rules, in general

Any equality of the form $eq : ∀\ x₁\ …\ xₖ → f\ p₁\ …\ pₙ ≡ v$ can be used as a rewrite rule, provided:

• $p₁ … pₙ$ are patterns
• $p₁ … pₙ$ are linear in $x₁ … xₖ$
• $f\ p₁\ …\ pₙ$ and $v$ have the same type
• $f\ p₁\ …\ pₙ$ does not reduce

## Higher-order patterns

Patterns can be higher order Miller patterns:

postulate
rew₁ :                 f (λ x → x)             ≡ t₂
rew₂ : ∀ (y : T)     → f (λ x → y)             ≡ y
rew₃ : ∀ (q : T → T) → f (λ x → q x)           ≡ q t₃
rew₄ : ∀ (y : T)     → h (λ (p : T → T) → p y) ≡ y

{-# REWRITE rew₁ rew₂ rew₃ rew₄ #-}


Miller fragment: Each pattern variable must be applied to distinct bound variables

## Other extensions of rewriting

• Non-linear rewrite rules
• Rewriting modulo $η$-equality
• Rewriting modulo irrelevance
• Rewriting in parametrized modules
• Rewriting universe-polymorphic functions
• Rewriting in presence of metavariables

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


# Conclusion

## Unchaining the power of computation

With the power of rewrite rules, you can:

• make more terms typecheck without annotations
• extend type theory with new constructions

You can start using it today!

https://wiki.portal.chalmers.se/agda

https://jesper.sikanda.be/publications.html