A Final Remark on scanr

scanr-pf 的 return type 其實可以復用 Logic.Identity module 裡面的 "_≡_" 和 scm 老師定義的 "_⋮_"：

scanr-pf' : {A B : Set} -> (f : A -> B -> B) -> (e : B) -> (xs : List A) ->
              List B ⋮ _≡_ ((map (foldr f e) ○ tails) xs)
scanr-pf' f e xs = sub ((foldr (sc f) (e :: [])) xs)
  ( chain> (map (foldr f e) ○ tails) xs
       === foldr (sc f) (e :: []) xs
             by foldr-fusion {_}{_}{_}
                  {til}{[] :: []}{map (foldr f e)}{sc f} fuse-cond xs
  ) where
    fuse-cond : {A B : Set}{f : A -> B -> B}{e : B} ->
                  (x : A)(yss : List (List A)) ->
                  map (foldr f e) (til x yss) ≡ (sc f) x (map (foldr f e) yss)
    fuse-cond x (ys :: yss) = refl

如此就不需要另外造一個 Indeed type，看起來也比較清楚。引進 _⋮_ 的 elimination rule，就可以導出較快的 scanr 版本：

subElim : {A : Set}{P : A -> Set} -> A ⋮ P -> A
subElim (sub x _) = x

scanr' : {A B : Set} -> (A -> B -> B) -> B -> List A -> List B
scanr' f e xs = subElim (scanr-pf' f e xs)

再這樣下去，Agda 就要變成我在 functional programming 上的母語了 XD。

--
我的名字悄悄出現在 scm 老師的網頁上了耶！XD