小玩

看過 scm 老師的 code，覺得 Balanced 定義成

prop Balanced :: Parity ~> Nat ~> Nat ~> *0 where
  Base :: Balanced Even Z Z
  EvenStep :: Balanced Even m n -> Balanced Even (S m) (S n)
  OddStep :: Balanced Even m n -> Balanced Odd (S 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) 

是完全依照 insert 的脈絡寫的，亦即如何對一棵已平衡的樹插入一個元素並保持平衡（hence the names for the value constructors），第一個版本感覺上比較 "general"。型驗（typecheck，我臨時掰出來的譯詞 XD）insert 時，我的 Balanced 乃為它量身打造，自然沒問題；但意義比較「好」的那版本卻在

insert x (Bin Odd  t u) = Bin Even t (insert x u)

這個 pattern 上吃癟，因為既有的假設是 Balanced Odd m n、要驗證的 constraint 是 Balanced Even m (S n)，但 Omega 手中預設的推導規則（i.e., axioms）是直接把 value constructor(s) 顛倒過來，所以只有

Balanced Even Z Z --> []
Balanced Even (S m) (S n) --> [Balanced Even m n]
Balanced Odd (S m) n --> [Balanced Even m n]

這三條，無論如何無法接上假設。解決之道只有引入其他推導規則，例如

Balanced Even m (S n) --> [Balanced Odd m n]

…其實我本來只打算留下殘局，可是寫到這裡突然想到〈Omega Users' Guide〉應該會有引進此類規則的機制。（否則何必在 trace 時特別把那些規則標示為 axioms 呢！）這傳說中的機制果然存在：section 20.1 "Types as Back-chaining Rules"！只要引進下面這個 theorem：

odd2even :: Balanced Odd m n -> Balanced Even m (S n) 
odd2even (OddStep substep) = EvenStep substep 

theorem odd_insert = odd2even

便可自 Balanced Even m (S n) 推得 Balanced Odd m n、接上假設 ─ check！

邊想邊寫效果還真不錯，所以在此順便推薦 literate programming！XD

--
睡了 XD。