Thinking Functionally with Haskell勉強メモ: 第６章２ foldr

foldr関数

sum、concat、filter、mapは似ている。

• リストを受け取る
• 空リストが停止条件
• (x:xs)が引数の場合、（mapやfilterの場合は何か関数適用した）xと、xsに対して再帰的処理した結果とを、なんらかの方法で結合する。

そして例えばsum (xs ++ ys) = sum xs + sum ysなどの法則を数学的帰納法で証明するのも同じ。

この共通性を抽象化し、特定の条件が満たされれば帰納法的な法則が成り立つと証明できるfoldr関数を定義する。

sumやmapなどをfoldrを使って定義できれば、帰納法を直接使うことなく「特定の条件を満たしている」と証明してfoldrの性質を使うだけでsum (xs ++ ys) = sum xs + sum ys`が証明できるようになる。

以下がfoldrの定義：

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f e [] = e
foldr f e (x:xs) = f x (foldr f e xs)

何が起きているのかを@という架空の演算子を例に紹介すると：

foldr (@) e [x, y, z] = x @ (y @ (z @ e))

となる。具体的には：

sum = foldr (+) 0
concat = foldr (++) []
map f = foldr ((:).f) []
filter p = foldr (\x xs -> if p x then x:xs else xs) []

面白いと思った点が二つ。

まず、((:) . fという関数合成。いままでは：

f :: (a -> b)
g :: (c -> a)
f . g :: (c -> b)

といった、引数が一つの関数を合成するのがすべてだったが、(:) . fは：

(:) :: a -> [a] -> [a]
f :: (b -> a)
(:) . f :: b -> [a] -> [a]

と「fが第一引数に適用される」という意味での関数合成になっている。

もう一つは：

filter p = foldr (\x xs -> if p x then x:xs else xs)

これは本当に何が起きてるか手書きで確かめるまで全然わからなかった。手で式をいじっていると納得するのだが。

F (xs ++ ys) = F xs @ F ys

さて、それではこのfoldrの定義を元に、どのような条件下で

foldr f e (xs ++ ys) = foldr f e xs @ foldr f e ys

が成立するかを帰納法で「証明」しながら見てみよう。（@の意味合いが先ほどと少し違っていることに注意）

Case [] 左辺

foldr f e ([] ++ ys)

= {[] ++ ys = ys}
foldr f e ys

Case [] 右辺

foldr f e [] @ foldr f e ys

= {foldr f e [] = e}
e @ foldr f e ys

foldr f e ysをxに置き換えたとして、F (xs ++ ys) = F xs @ F ysが成り立つための条件の一つはx = e @ xだとわかる。

Case x:xs 左辺

foldr f e ((x:xs) ++ ys)

= {(x:xs) ++ ys = x:(xs ++ ys)}
foldr f e (x:(xs ++ ys))

= {foldr f e (x:xs) = f x (foldr f e xs)}
f x (foldr f e (xs ++ ys))

= {induction}
f x (foldr f e xs @ foldr f e ys)

Case x:xs 右辺

foldr f e (x:xs) @ foldr f e ys

= {foldr f e (x:xs) = f x (foldr f e xs)}
(f x (foldr f e xs)) @ foldr f e ys

foldr f e xsをy、foldr f e ysをzに置き換えるとf x (y @ z) = (f x y) @ zがもう一つの条件だとわかる。

つまり：

x = e @ x
f x (y @ z) = (f x y) @ z

を満たせば

foldr f e (xs ++ ys) = foldr f e xs @ foldr f e ys

が成り立つ。

例えばf = (@)、(@)が結合律を満たし、eが(@)の単位元であれば二つの条件は満たされる。

sumとconcatの場合は(f, @, e)で(+), (+), 0と(++), (++), []で条件が満たされている。

map gに関しては(f, @, e)が( (:).g, (++), [] )なので

x = [] ++ x
(g x) : (y ++ z) = ((g x):y) ++ z

でどちらも++の定義と同型なので成り立つ。

filter pがややこしい。

For the law of filter we require that

if p x then x:(ys++zs) else ys++zs

= (if p x then x:ys else ys) ++ zs

This is immediate from the definitions of concatenation and conditional expressions. (TFwH p119-120)

って読んだ時：

“This is immediate from the definitions of concatenation and conditional expressions”? if式の定義ってどっかに書いてた？読み返したり索引見ても見つからないが…

— zehnpaard (@zehnpaard) 2018年3月22日

ifみたいな分岐でどう証明するのかってまだ全然例が出てないから「自明」じゃないと思うのだが…

— zehnpaard (@zehnpaard) 2018年3月22日

こういう気持ちになった。

conditional expressionの定義は多分

if True then a else b = a
if False then a else b = b

なので

Case True 左辺

if True then (xs++zs) else (ys++zs)

= {conditional expressionの定義}
xs++zs

Case True 右辺

(if True then xs else ys) ++ zs

= {conditional expressionの定義}
xs++zs

Case False 左辺

if False then (xs++zs) else (ys++zs)

= {conditional expressionの定義}
ys++zs

Case False 右辺

(if False then xs else ys) ++ zs

= {conditional expressionの定義}
ys++zs

で証明完了。必要な

if p x then x:(ys++zs) else ys++zs
   = (if p x then x:ys else ys) ++ zs

が導き出せる。

Fusion

foldrの性質で最も重要なものは

f . foldr g a = foldr h b

という関数合成に関するもの。各変数が特定の条件を満たしている必要がある。

例えば

double . sum = foldr ((+) . double) 0
length . concat = foldr ((+) . length) 0

となる。（length . concatは（直感的には意味がわかるものの）concatがfoldr (++) []なことを考えると少し不思議に見える。）

この関数合成関連のFusion則を使うと、前回帰納法で証明してきたような法則の多くは簡単に導き出せてしまう、とのこと。

Fusion則が成り立つために各部分が満たさなければいけない条件を調べる。

Case undefined 左辺

f (foldr g a undefined)

= {foldr x y undefined = undefined}
f undefined

Case undefined 右辺

foldr h b undefined

= { foldr x y undefined = undefined}
undefined

なのでf undefined = undefined、つまりfがstrictであるのが条件の一つ。

Case [] 左辺

f (foldr g a [])

= {foldrの定義}
f a

Case [] 右辺

foldr h b []

= {foldrの定義}
b

なのでf a = bも条件。

Case x:xs 左辺

f (foldr g a (x:xs))

= {foldrの定義}
f (g x (foldr g a xs))

Case x:xs 右辺

foldr h b (x:xs)

= {foldrの定義}
h x (foldr h b xs)

= {induction}
h x (f (foldr g a xs))

foldr g a xsをyに置き換えてf (g x y) = h x (f y)が最後の条件。

まとめると

f . foldr g a = foldr h b

が成り立つには：

f undefined = undefined
f a = b
f (g x y) = h x (f y)

の三つが条件（最後の条件は任意のxとyで成立しなければいけない）。

さて、このfusion則から

foldr f a . map g = foldr h a

を導き出したい。

map g = foldr ((:) . g) []なので

foldr f a . foldr ((:) . g) [] = foldr h a

で（少々ややこしいことに）

f_fusion = foldr f a
g_fusion = (:) . g
a_fusion = []
h_fusion = h
b_fusion = a

上記のようにfusion則の変数と対応させることになる。正直ここらへんはHaskellの一文字変数の不便さが出ているようにも思う。

この対応付けでfusion則の第一、第二条件は：

foldr f a undefined = undefined
foldr f a [] = a

となり、どちらも満たされていることが確認出来る。

第三条件は

foldr f a (((:) . g) x y) = h x (foldr f a y)

となり、左辺が

foldr f a (((:) . g) x y)

=
foldr f a ((g x): y)

=
f (g x) (foldr f a y)

foldr f a yをzで置き換えるとf (g x) y = h x yになる。あるいはh = f . g。

つまり

foldr f a . map g = foldr (f . g) a

という法則が導き出される。

この法則によりdouble . sumは

double . sum 

= 
sum . map double

= 
foldr (+) 0 . map double

=
foldr ((+) . double) 0

length . concatは

length . concat

=
sum . map length

=
foldr (+) 0 . map length

=
foldr ((+) . length) 0

と書いてあるのだが、length . concat = sum . map lengthはどこからきたんだ？

便利だとは思うが、微妙に論理の飛躍が感じられあまり釈然としない・・・