I'm teaching myself about dependent types by learning Agda.
Here's a type for 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))
A tree can either be completely balanced (bal
), or the left subtree could contain one more element than the right subtree (heavyL
). (In that case, the next insertion would go into the right subtree.) The idea is that insertions would flip between the left and right halves of the tree, effectively (deterministically) shuffling an input list.
I can't make this definition of insert
typecheck:
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 rejects bal l (insert x r)
as the right-hand side of the heavyL
case:
.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 attempted to patch up my definition with a proof...
insert x (heavyL {n} l r) rewrite +-suc n n = bal l (insert x r)
... but I get the same error message. (Have I misunderstood what rewrite
does?)
I 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 accepts this as a possibility, but highlights the equation in yellow. I figured I need to explicitly give the size of the two subtrees that I was passing to the bal
constructor:
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'm out of ideas. I'm sure I've made a stupid mistake. What am I doing wrong? What do I need to do to make my definition of insert
typecheck?
You just need to rewrite in the another direction:
You can use Agda's great hole machinery to figure out what's going on:
after typechecking and placing the cursor inside
{!!}
, you can typeC-c C-,
and getAfter placing
bal l (insert x r)
in the hole and typingC-c C-.
you'll getSo there is a mismatch.
rewrite
fixes it:Now typing
C-c C-.
(after typechecking) givesand you can finish the definition by typing
C-c C-r
in the hole.Agda can't infer
n
andm
fromn + suc m
, because there is pattern matching onn
. There was a thread about implicit arguments on the Agda mailing list.