Statically balanced trees in Agda
I teach myself about dependent types by studying Agda.
Here is a type of binary trees, balanced by their size.
open import Data.Nat
open import Data.Nat.Properties.Simple
data T (A : Set) : ℕ -> Set where
empty : T A 0
leaf : A -> T A 1
bal : ∀ {n} -> T A n -> T A n -> T A (n + n)
heavyL : ∀ {n} -> T A (suc n) -> T A n -> T A (suc (n + n))
The tree can be fully balanced ( bal
), or the left subtree can contain one more element than the right subtree ( heavyL
). (In this case, the next insert will fall into the right subtree.) The idea is that the inserts will flip between the left and right halves of the tree, effectively (deterministically) shuffling the input list.
I cannot make this insert
typecheck definition :
insert : ∀ {A n} -> A -> T A n -> T A (suc n)
insert x empty = leaf x
insert x (leaf y) = bal (leaf x) (leaf y)
insert x (bal l r) = heavyL (insert x l) r
insert x (heavyL l r) = bal l (insert x r)
Agda dismisses bal l (insert x r)
as the right side of the case heavyL
:
.n + suc .n != suc (.n + .n) of type ℕ
when checking that the expression bal l (insert x r) has type
T .A (suc (suc (.n + .n)))
I tried to fix my definition with proof ...
insert x (heavyL {n} l r) rewrite +-suc n n = bal l (insert x r)
... but I get the same error message. (I didn't understand what it was doing rewrite
?)
I've also tried converting trees of equivalent sizes under the same proof assumption:
convertT : ∀ {n m A} -> T A (n + suc m) -> T A (suc (n + m))
convertT {n} {m} t rewrite +-suc n m = t
insert x (heavyL {n} l r) rewrite +-suc n n = bal (convertT l) (convertT (insert x r))
Agda takes this as an opportunity, but highlights the equation in yellow. I decided that I needed to explicitly specify the size of the two subtrees that I passed to the constructor bal
:
insert x (heavyL {n} l r) rewrite +-suc n n = bal {n = suc n} (convertT l) (convertT (insert x r))
But now I get the same error message again!
n + suc n != suc (n + n) of type ℕ
when checking that the expression
bal {n = suc n} (convertT l) (convertT (insert x r)) has type
T .A (suc (suc (n + n)))
I have no idea. I'm sure I made a dumb mistake. What am I doing wrong? What do I need to do to make my insert
typecheck definition ?
source to share
You just need to rewrite in the other direction:
open import Relation.Binary.PropositionalEquality
insert : ∀ {A n} -> A -> T A n -> T A (suc n)
insert x empty = leaf x
insert x (leaf y) = bal (leaf y) (leaf y)
insert x (bal l r) = heavyL (insert x l) r
insert x (heavyL {n} l r) rewrite sym (+-suc n n) = bal l (insert x r)
You can use Agda's dedicated hardware to determine what's going on:
insert x (heavyL {n} l r) = {!!}
after checking the types and placing the cursor inside {!!}
, you can type C-c C-,
and get
Goal: T .A (suc (suc (n + n)))
————————————————————————————————————————————————————————————
r : T .A n
l : T .A (suc n)
n : ℕ
x : .A
.A : Set
Once placed bal l (insert x r)
in the hole and inserted, C-c C-.
you will receive
Goal: T .A (suc (suc (n + n)))
Have: T .A (suc (n + suc n))
————————————————————————————————————————————————————————————
r : T .A n
l : T .A (suc n)
n : ℕ
x : .A
.A : Set
So there is a mismatch. rewrite
fixes this:
insert x (heavyL {n} l r) rewrite sym (+-suc n n) = {!bal l (insert x r)!}
Now typing C-c C-.
(after type checking) you get
Goal: T .A (suc (n + suc n))
Have: T .A (suc (n + suc n))
————————————————————————————————————————————————————————————
r : T .A n
l : T .A (suc n)
x : .A
.A : Set
n : ℕ
and you can end the definition by typing C-c C-r
in the hole.
Agda takes this as a possibility, but highlights the equation in yellow.
Agda cannot infer to n
and m
from n + suc m
because there is pattern matching on n
. There was a thread about implicit arguments on the Agda mailing list.
source to share
Your attempt rewrite
almost works, but the equality it uses is going in the wrong direction. To make it work in the right direction, you can flip it:
open import Relation.Binary.PropositionalEquality
-- ...
insert x (heavyL {n} l r) rewrite sym (+-suc n n) = bal l (insert x r)
or use the suggestion with
:
insert x (heavyL {n} l r) with bal l (insert x r)
... | t rewrite +-suc n n = t
Another possibility is to do the substitution yourself on the right side:
open import Relation.Binary.PropositionalEquality
-- ...
insert x (heavyL {n} l r) = subst (T _) (+-suc (suc n) n) (bal l (insert x r))
source to share