foldr をやっと正しく理解した

今まで foldr についていい加減な理解をしていたが、やっと正しく理解できた(気がする)。理解できていなかったのは、無限リストに適用しても停止する(ことがある)のは何故かというところ。

よくある例

Prelude.and を foldr と (&&) を使って作ってみる。foldr と (&&) を使うと False を見つけて時点で処理を打ち切ることができて効率が良い。無限リストであっても False が含まれてさえいれば停止する。foldl だとこうはいかない。

and' :: [Bool] -> Bool
and' = foldr (&&) True

なぜ foldr だと無限リストでも停止するのか

疑問

foldr は右からの畳み込みだ。例えば [False, True, True] に上で作った and' を適用したとするとこうなるはず。

  and ' [False, True, True]
= foldr (&&) True [False, True, True]
= (False && (True && (True && True)))
= False

右からの畳み込みだから、最後の要素がわからないと計算できないはず。例は有限の要素だから停止するのは理解できるが、無限リストでも停止するのはなぜだろう。無限リストは最後の要素が何かはわからない。

(&&) の定義

(&&) は次のように定義されている。

True  && x = x
False && _ = False

1 つ目の引数が True ならば 2 つ目の引数を返す。1 つ目の引数が False ならば 2 つ目の引数は評価せずに False を返す。この 1 つ目の引数が False のパターンが効いてくる。

foldr の定義

foldr の定義を見るとなぜ途中をすっ飛ばすのか、無限リストでも停止するのかがわかった。定義は次のようになっている。

foldr k z = go
  where
    go []     = z
    go (y:ys) = y `k` go ys

k を (&&) とした場合、y が True であれば go ys の結果を返す (True && x = x より)。y が False であれば go ys を評価せずに False を返す (False && _ = False より)。よって ys が無限リストであっても評価されないので、プログラムは停止する。遅延評価のおかげだ。

まとめ

  • foldr 自体が無限リストに対応しているわけではない。
  • foldr に渡す関数によっては無限リストに適用しても停止する可能性がある。
  • ソースを読め。