5.4 變數換常數

接下來的幾節中，我們將介紹幾種常見的程式推導技巧。 \todo{generalize}

本節先以一個簡單但時常用上的技巧作為開頭。 回顧在例 [RefUndefined] 中提及的函數 positions:

positions z = map fst . filter ((==z) . snd) . zip [Zero..] 

positions z xs 傳回 z 在 xs 中出現的所有位置。 上述的定義方式會產生許多中間串列。 我們能用第 5.1 節中的方式，利用展開-收回轉換為 positions 推導出一個歸納定義，並藉此將中間串列消除嗎？

我們針對 positions z 的輸入做分析， 在歸納狀況中，先將 positions z (x:xs) 展開，希望最後能收回 positions z xs. 由於讀者對相關計算應已熟悉，以下的演算以較快的步調進行：

      positions z (x:xs)
 ===  map fst . filter ((==z) . snd) . zip [Zero .. ] $ (x:xs)
 ===    {- zip 之定義， [0..] = 0 : [1..] -}
      map fst . filter ((==z) . snd) $ (Zero,x) : zip [1..] (x:xs)
 ===    {- map 與 filter 之定義 -}
      if x==z then Zero : map fst (filter ((==z) . snd) (zip [1..] (x:xs)))
         else map fst (filter ((==z) . snd) (zip [1..] (x:xs))) 

結果我們卡在這兒了：最後的式子中，zip 的參數是 [1..], 但 positions 的定義要求這個參數得是 [Zero ..]. 我們無法將式子收回得到 positions z xs.

看來，問題是 positions 的定義把 Zero 給寫死了。如果我們索性把該位置變成一個變數呢？ 我們定義：

posFrom z i = map fst . filter ((z==) . snd) . zip [i..]

函數 positions 是 posFrom 的特例：positions z = posFrom z 0. 而 posFrom 的歸納定義可用展開-收回轉換找出：

      posFrom z i (x:xs)
 ===  map fst . filter ((==z) . snd) . zip [i..] $ (x:xs)
 ===    {- zip 之定義， [i..] = i : [Suc i..] -}
      map fst . filter ((==z) . snd) $ (i,x) : zip [Suc i..] (x:xs)
 ===    {- map 與 filter 之定義 -}
      if x==z then i : map fst (filter ((==z) . snd) (zip [Suc i..] (x:xs)))
         else map fst (filter ((==z) . snd) (zip [Suc i..] (x:xs)))
 ===    {- posFrom 之定義 -}
      if x==z then i : posFrom z (Suc i) xs
         else posFrom z (Suc i) xs 

由此我們可得：

posFrom z i []      =  []
posFrom z i (x:xs)  =  if x==z then i : posFrom z (1+i) xs
                         else posFrom z (1+i) xs 

由於將一個常數換成變數，posFrom 比 positions 多了些彈性，因此較容易收回。 這個技巧在許多場合用得上，往往是許多程式推導的第一步。 但我並不建議大家看到任一個定義，便一股腦地把所有常數都換成變數。 如同第2.7 節中提及的原則，該把哪些常數換掉仍應由計算中發現，只用在必要之處。

index :: List a -> List (Nat × a)
index = zip [Zero .. ] 

     index (x:xs)
 === zip [Zero .. ] (x:xs)
 ===  {- [Zero ..] = Zero: [1 ..], zip 之定義 -}
     (Zero,x) : zip [1..] xs 

indexFrom :: Nat -> List a -> List (Nat × a)
indexFrom i = zip [i..] 

     indexFrom i (x:xs)
 === zip [i .. ] (x:xs)
 ===  {- [i ..] = i: [Suc i ..], zip 之定義 -}
     (i,x) : zip [Suc i..] xs
 === (i,x) : indexFrom (Suc i) xs 

indexFrom i []      = []
indexFrom i (x:xs)  = i,x) : indexFrom (Suc i) xs