Type Theory Unchained

PLNL 2019 in Nijmegen

Jesper Cockx

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.

Should definitional equality be extensible or algorithmic?

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

Taming your rewrite rules

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

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