みじめな妥協策としては

http://www.iis.sinica.edu.tw/~scm/2007/agda-exercise-length-indexed-mergesort/
via http://twitter.com/ikegami__/status/3573974552

いけがみさんの一言でクイックソートはどうでも良いっていうか、この周辺に4日ぐらい居た気がして、その間他の事があんまり出来なかったけど、分からんなーとか言いまくりながら小説読めてたので結果的に良かったです。

それで、URLで頑張ってるみたくSizedListや、Sized-Baranced-Treeを作らなくても

-- ソート済みの二つのリストを合併して、新しく１つのソート済みのリストを作る
-- 普通
Merge : List Nat -> List Nat -> List Nat
Merge [] y = y
Merge x [] = x
Merge (x :: xs) (y :: ys) = if x < y then (x :: (Merge xs (y :: ys))) else (y :: (Merge (x :: xs) ys))

-- 残念なマージソート
-- 要素数が2個以上の時は、headとtailにわけて tailをマージソート。更にその結果をマージする
-- これで全体としてはソート済みを保っている
MergeSort : List Nat -> List Nat
MergeSort [] = []
MergeSort (x :: []) = (x :: [])
MergeSort (x :: xs) = Merge (x :: []) (MergeSort xs)

シンプルにこうやってやれば出来そうで、ただまぁ・・・酷過ぎるかなーとかは。

型コンストラクタをベースにした、構成に関する帰納法的な感じだと思うので、多分、「木にしておく」っていうのは有効な手なんじゃないかなーとかは。いや・・・どうだろう・・・。まぁそれは置いておいて。

上のURLの中で面白いのは

_+_ : Nat -> Nat -> Nat
zero + b = b
(succ a) + b = succ (a + b)

という加算の定義をした上で

lemma1
任意のn,mについて、(succ n) + m と succ (n + m) が等しい事を示す。

lemma2
任意のn,mについて n + (succ m) と (succ n) + m が等しい事を示す。

lemma3
任意のn,mについて n + (succ m) と succ (n + m) が等しい事を示す。

などをやっておかないと

insert : {A : Set0} -> {n : Nat} -> A -> Tree A n -> Tree A (succ n)
insert x Nul = Tip x
insert x (Tip y) = Bin Even (Tip x) (Tip y)
insert x (Bin Even t u) = Bin Odd (insert x t) u
insert {A} x (Bin {n} Odd t u) = Bin Even t (insert x u)

において、最後の節で

返値の型がTree A (succ ((parity Odd) + (n + n)))となって、
parity Oddから
Tree A (succ ((succ zero) + (n + n)))
_+_の定義から
Tree A (succ (succ (zero + (n + n))))
更に
Tree A (succ (succ (n + n))

一方、Bin Even t (insert x u)では
Tree A (parity Even + ((succ n) + (succ n)))
となり、parity Evenより
Tree A (zero + ((succ n) + (succ n)))
_+_の定義から
Tree A ((succ n) + (succ n))
更に
Tree A (succ (n + (succ n))
となり

Tree A (succ (succ (n + n))) と Tree A (succ (n + (succ n))) が unifyされようとするのですが
(succ (n + n)) == (n + (succ n))が分からないので

(succ (n + n)) != (n + (succ n))

だとか言われてしまいます。

もっとも、(Agda2の中で)示さなくても、公準を用いて

postulate Same : {A : Set0} -> {n : Nat} -> Tree A (succ (n + succ n)) -> Tree A (succ (succ (n + n)))

...

insert {A} x (Bin {n} Odd t u) = Same (Bin Even t (insert x u))

とかやってしまえば、まぁ型だけは合わせられるんですけれども。

この辺は凄く面白かった。