Statically-Checked Balanced Tree

首先是一些基本定義和定理。

plus :: Nat ~> Nat ~> Nat
{plus Z y} = y
{plus (S x) y} = S {plus x y}

assoc :: Nat' x -> Equal {plus x (S y)} {plus (S x) y}
assoc Z = Eq
assoc (S x) = Eq where theorem indHyp = assoc x

theorem associativity = assoc

接著是 Parity kind 和相對應的 singleton type Parity' 的定義。我照著〈Putting Curry-Howard to Work〉的語法在 Parity 定義後寫 deriving Singleton Parity' 可是不 work，所以手工定義一個。

kind Parity = Even | Odd

data Parity' :: Parity ~> *0 where
  Even :: Parity' Even
  Odd :: Parity' Odd

再來是 static proposition Balanced。令左子樹大小為 m、右子樹大小為 n、節點的 parity 為 p，命題 Balanced p m n 是說，m、n 符合平衡的定義（i.e., m = n + 1 or m = n），而且在此節點上的 parity p 是對的。定義是 by induction。比較奇怪的地方是，定義裡面沒有明確指出 m = n + 1 or m = n，但此事可以從這個定義簡單歸納推得。

prop Balanced :: Parity ~> Nat ~> Nat ~> *0 where
  Base :: Balanced Even Z Z
  InsLeft :: Balanced Even m n -> Balanced Odd (S m) n
  InsRight :: Balanced Odd m n -> Balanced Even m (S n)

最後是 Tree 和 insert 的定義。

data Tree :: *0 ~> Nat ~> *0 where
  Nul :: Tree a Z
  Tip :: a -> Tree a (S Z)
  Bin :: Balanced p m n =>
         Parity' p -> Tree a m -> Tree a n -> Tree a {plus m n}
  
insert :: a -> Tree a n -> Tree a (S n)
insert x Nul = Tip x
insert x (Tip y) = Bin Even (Tip x) (Tip y)
insert x (Bin p t u) = case p of
  Even -> Bin Odd (insert x t) u
  Odd -> Bin Even t (insert x u)

最需要 defend 的地方應該是 Bin constructor 是不是足以證明樹是平衡的。scm 老師在我寫 p 的地方都寫 {parity {plus m n}}，其中 parity :: Nat ~> Parity，但這樣似乎需要另外給不少定理。我目前看覺得沒問題，因為 p 被 Balanced p m n 所限制，不能亂給。

--
Balanced 應該還有別的表述方法。

---

不過直接使用 Bin 時發生一些問題，目前無法解決。狀況是：

prompt> insert 1 (insert 2 (insert 3 (insert 4 (insert 5 Nul))))
(Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 3)) (Tip 4)) (Bin Even (Tip 2) (Tip 5))
) : Tree Int 5t

但如果在源碼內加入

t = (Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 3)) (Tip 4)) (Bin Even (Tip 2) (Tip 5)))

就會導致

While type checking: t
Under the truths: 
We tried to solve: Balanced Odd {plus {plus 1t 1t} 1t} {plus 1t 1t},Balanced Odd
 {plus 1t 1t} 1t
But we were left with: Balanced Odd {plus 1t 1t} 1t, Balanced Odd {plus {plus 1t
 1t} 1t} {plus 1t 1t}
The proposition: (Balanced Odd {plus 1t 1t} 1t) is refutable.

或是像這樣直接在 interpreter 下說：

prompt> let t2 = insert 4 (insert 5 Nul)
t2 
prompt> t2
(Bin Even (Tip 4) (Tip 5)) : Tree Int 2t
prompt> let t3 = insert 1 (insert 2 (insert 3 Nul))
t3 
prompt> t3
(Bin Odd (Bin Even (Tip 1) (Tip 2)) (Tip 3)) : Tree Int 3t
prompt> Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 2)) (Tip 3)) (Bin Even (Tip 4) (
Tip 5))
Unresolved obligations:
  Balanced Odd 3t 2t => Tree Int 5t
prompt> Bin Odd t3 t2
(Bin Odd (Bin Odd (Bin Even (Tip 1) (Tip 2)) (Tip 3)) (Bin Even (Tip 4) (Tip 5))
) : Tree Int 5t

最後這段我實在傻眼了 XD。

--
有盲點？

---

我打開追蹤模式 check 很長的那一串，更令人費解。最後一步是

Trying to find evidence for the predicate:
   Balanced Odd 3t 2t
Under assumptions:
   []
Currently solving subproblems from the rules: Base,InsLeft,InsRight,InsLeft,Base
,InsLeft,InsRight,Base,InsLeft,InsRight
Possibly matching rules are
  Axiom InsRight(Balanced): [] => Balanced Even 'a (1+'b)t --> [Balanced Odd 'a 
'b],
  Axiom InsLeft(Balanced): [] => Balanced Odd (1+'c)t 'd --> [Balanced Even 'c '
d],
  Axiom Base(Balanced): [] => Balanced Even 0t 0t --> []

press return to step, 'c' to continue:


Exactly 0 rules match:
  

Unresolved obligations:
  Balanced Odd 3t 2t => Tree Int 5t

對照組：我改而 check Bin Odd t3 t2，前兩步是：

Trying to find evidence for the predicate:
   Balanced Odd 3t 2t
Under assumptions:
   []
Currently solving subproblems from the rules: 
Possibly matching rules are
  Axiom InsRight(Balanced): [] => Balanced Even 'a (1+'b)t --> [Balanced Odd 'a 
'b],
  Axiom InsLeft(Balanced): [] => Balanced Odd (1+'c)t 'd --> [Balanced Even 'c '
d],
  Axiom Base(Balanced): [] => Balanced Even 0t 0t --> []

press return to step, 'c' to continue:


Rule : InsLeft
Matched term: Balanced Odd 3t 2t
 Rewrites to: Balanced Even 2t 2t
 Under subst: {e=2t, f=2t}
Prerequisite: 

Exactly 1 rules match:
  


Trying to find evidence for the predicate:
   Balanced Even 2t 2t
Under assumptions:
   []
Currently solving subproblems from the rules: InsLeft
Possibly matching rules are
  Axiom InsRight(Balanced): [] => Balanced Even 'a (1+'b)t --> [Balanced Odd 'a 
'b],
  Axiom InsLeft(Balanced): [] => Balanced Odd (1+'c)t 'd --> [Balanced Even 'c '
d],
  Axiom Base(Balanced): [] => Balanced Even 0t 0t --> []

press return to step, 'c' to continue:

--
我放棄了…