Counting Sort

〈Functional Algorithm Design〉最後一節的那三個 sorting algorithm derivation 實在好複雜，所以我想自己弄一個試試看。於是我挑上

perm : List Nat ← List Nat
perm = ((fun bagify) º) ○ (fun bagify)

這個定義來做。其中 bag 實作為一個 List (Nat × Nat)，每個 pair 分別是一個數字和它出現的次數，整個 list 依照前者從小到大排列。（就是這裡作弊了 XD。）bagify 就定義成

bagify : List Nat -> List (Nat × Nat)
bagify = foldr consbag []
  where
    consbag : Nat -> List (Nat × Nat) -> List (Nat × Nat)
    consbag a [] = < a , 1 > :: []
    consbag a (< a' , c > :: x) =
        a == a' => < a' , suc c > :: x
      ! a >  a' => < a' ,     c > :: consbag a x
      ! otherwise  < a , 1 > :: < a' , c > :: x

把 specification ordered? ○ perm 展開成 ordered? ○ bagifyº ○ bagify 後，很顯然只能從前面兩個下手，而那一段很自然就是把 bag 鋪展成一個 sorted list。把這個動作叫做 unroll，

unroll : List (Nat × Nat) -> List Nat
unroll = foldr dup []
  where
    dup : Nat × Nat -> List Nat -> List Nat
    dup < a , c > x = dup-term a c x
      where
        dup-term : Nat -> Nat -> List Nat -> List Nat
        dup-term a      0  x = x
        dup-term a (suc n) x = a :: dup-term a n x

就得到 counting sort unroll ○ bagify。雖然整個 derivation 平淡無奇，也沒用到 fold fusion，不過在其他 sorting 都還做不出來的情況下，先來試試也好 XD。

--
像 combine = cons ⊔ (cons ○ (idR ⨉ combine) ○ swap ○ (idR ⨉ (cons º))) 這種 relation 根本沒辦法動它呀 XD。