我敢發誓

我寫的 Maximum Segment Sum 一定是對的！

好吧，上面只是廣告詞，因為我還沒把 MSS 證完 XD。不過證明的技巧已經用在 scanr 上面，看起來很成功 XD。

接續上篇，為了找到實用例子，我決定拿經典的 MSS 問題開刀。順帶一提，上篇和這篇都是參考 scm 老師的 lectures on program derivation XD。

先定義一些 MSS 會用到的簡單 functions，剛好都是 folds。（Int 定義在 Data.Integer module 裡面。）

max : List Int -> Int
max = foldr (\x y -> if x > y then x else y) (pos 0)

sum : List Int -> Int
sum = foldr _+_ (pos 0)

concat : {A : Set} -> List (List A) -> List A
concat = foldr _++_ []

inits : {A : Set} -> List A -> List (List A)
inits = foldr (\x xss -> [] :: map (_::_ x) xss) ([] :: [])

til : {A : Set} -> A -> List (List A) -> List (List A)
til x (ys :: yss) = (x :: ys) :: ys :: yss

tails : {A : Set} -> List A -> List (List A)
tails = foldr til ([] :: [])

下一個要寫的是 scanr，其定義是

naive-scanr : {A B : Set} -> (A -> B -> B) -> B -> List A -> List B
naive-scanr f e = map (foldr f e) ○ tails

這時 scm 老師就要說話了："Of course, it is slow to actually perform map (foldr f e) separately. By fold-fusion, we get a faster implementation." 所以先前證明的 Fold-Fusion Theorem（foldr-fusion function）即將粉墨登場！日前某次失敗設計裡面用到的 Indeed 現在終於找到自己的生存意義 XD，它讓 scanr-pf 得以保證傳回的值一定和 naive-scanr 一樣，但裡面的實作其實是經過 fold-fusion 所得到的較快版本。

data Indeed {A : Set} : A -> Set where
  indeed : (x : A) -> Indeed x

sc : {A B : Set} -> (A -> B -> B) -> A -> List B -> List B
sc f x (y :: ys) = f x y :: y :: ys

scanr-pf : {A B : Set} -> (f : A -> B -> B) -> (e : B) ->
          (xs : List A) -> Indeed ((map (foldr f e) ○ tails) xs)
scanr-pf f e xs = subst Indeed
  ( 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
  ) (indeed ((foldr (sc f) (e :: [])) 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

不幸的是，scanr-pf 實際上會跑得比 naive-scanr 還要慢，因為前者除了 term-level 的計算，還有 type-level 的計算，也就是說它還得額外跑一次 naive-scanr 來計算它的 return type！因此我們必須找個方法把這份其實不需要的 type information 擦掉。以下這個方法剛好可行：引入 Indeed 的 elimination rule，

indeedElim : {A : Set}{x : A} -> Indeed x -> A
indeedElim (indeed x) = x

經過加速而且保證正確的 scanr 就現身了！

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

最後是 naive-mss 的定義。naive-mss 跑得非常慢，長度 8 的 array 就不知道跑到哪裡去了 XD。

naive-mss : List Int -> Int
naive-mss = max ○ map sum ○ concat ○ map inits ○ tails

只要依循「scanr 模式」，只花線性時間而且保證正確的 mss function 也可以寫得出來。不過 MSS 的 derivation 實在有點長，所以就先放著，反正原則就是那樣 XD。

-- mss-pf : (xs : List Int) ->
--            Indeed ((max ○ map sum ○ concat ○ map inits ○ tails) xs)
-- mss-pf xs = subst Indeed ? ?

-- mss : List Int -> Int
-- mss = indeedElim ○ mss-pf  -- this may not typecheck

--
以上都是偷寫的，真的要就此打住了 XD。