foldr で dropWhile を再定義する

Haskell の Prelude に定義されている関数を、高階関数をつかって再定義してみようという「プログラミング Haskell」第 7 章の問題について。

（folder は foldr の誤記）

それはともかく、こんなことを考えてみたり、

dropWhile'
 = \p -> foldl
  (\xs x -> let xs' = xs ++ [x] in if and . map p $ xs' then xs else xs')
  []

（これは間違い。　述語 p が成立する要素を取り除く逆 filter になってしまっている）

あるいは、次のように drop に渡す n を計算したりと、いろいろ苦労したんだけれど、どうにもきれいにまとまらなくて悶々としていた。

dropWhile' p xs = drop n xs where
 n = foldr f 0 (map p xs)
 f = \b -> if b then succ else const 0

（術後は述語の間違い）

しかーし今日！　頭上に電球ピコーン！級の回答を同僚から入手して感動さめやらない状態。
リファインした定義はこんな感じ。

dropWhile' p xs = foldr (\x ys -> if p x then tail ys else xs) [] xs

ためしに p に (<3) を、 xs に [1,2,3,1] を与えて簡約してみよう。

  dropWhile' (<3) [1,2,3,1]
= { dropWhile' の定義を展開 }
  (\p xs -> foldr (\x ys -> if p x then tail ys else xs) [] xs) (<3) [1,2,3,1]
= { 引数を適用 }
  foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [1,2,3,1]
= { foldr を一回適用 }
  (\x ys -> if (<3) x -> then tail ys else [1,2,3,1])
    1                                                                      -- x
    (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [2,3,1]) -- ys
= { 最初のλ式を引数に適用 }
  if (<3) 1
    then tail (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [2,3,1])
    else [1,2,3,1]
= { if (<3) 1 ... を評価 }
  tail (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [2,3,1])
= { foldr を再適用 }
  tail ((\x ys -> if (<3) x -> then tail ys else [1,2,3,1])
    2                                                                    -- x
    (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [3,1]) -- ys
    )
= { λ式を引数に適用 }
  tail (if (<3) 2 ->
    then tail (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [3,1])
    else [1,2,3,4]))
= { if 文を評価 }
  tail (tail (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [3,1]))
= { foldr を再適用}
  tail (tail ((\x ys -> if (<3) x -> then tail ys else [1,2,3,1])
    3                                                                  -- x
    (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [1]) -- ys
    ))
= { λ式を適用 }
  tail (tail (if (<3) 3 ->
    then tail (foldr (\x ys -> if (<3) x -> then tail ys else [1,2,3,1]) [] [1])
    else [1,2,3,1]))
= { if 文を評価 }
  tail (tail [1,2,3,1])
= { 二番目の tail を適用 }
  tail [2,3,1]
= { 再度 tail を適用 }
  [3,1]

ということで、たしかに期待した通りに簡約がすすむ。

わたした初期値を無視する fold に、述語に最初のリスト xs をバインドしておくこと、ふたつの点で「その発想はなかった！」 dropWhile 再定義でございました。