Thinking Functionally with Haskell勉強メモ: 第4章2 concat/map/filter、functorと自然変換、同一性の証明
リストに対する処理の性質・法則、Functorに対するの一般化、性質の証明法についてメモ:
まずはconcat
、map
、filter
の定義:
concat :: [[a]] -> [a] concat [] = [] concat (xs:xss) = xs ++ concat xss map :: (a -> b) -> [a] -> [b] map _ [] = [] map f (x: xs) = f x : map f xs filter :: (a -> Bool) -> [a] -> [a] filter _ [] = [] filter p (x:xs) | p x = x:filter p xs | otherwise = filter p xs --あるいは filter p = concat . map (test p) test p x = if p x then [x] else []
Functor laws of map
map
には以下の性質がある:
map id = id map (f . g) = map f . map g
これらをfunctor laws of mapという。map
はlist
に対して上記二点の性質を持つが、そのような性質を保つmap
に似た関数が定義されている他のデータ構造もありえる。
そのようなデータ構造の型クラスとしてFunctor
が用意されている:
class Functor a where fmap :: (b -> c) -> a b -> a c
list
の場合a b
とa c
が[b]
と[c]
に置き換えられて、fmap :: (b -> c) -> [b] -> [c]
でmap
の型に合致する。
fmap
もmap
の二つの性質をFunctor type classのInstanceに対して持つ(というかmap
はlist
に対するfmap
の別名)。
例えば二分木構造:
data Tree a = Tip a | Fork (Tree a) (Tree a) instance Functor Tree where fmap f (Tip x) = Tip (f x) fmap f (Fork u v) = Fork (fmap f u) (fmap f v)
Tree
型はFunctor
型クラスのInstanceで、fmap f
で葉ノードすべてにたいして関数fが適用される。
自然変換
map
に関する法則には他にもいくつか存在する:
f . head = head . map f -- この法則のみfはstrictである必要がある map f . tail = tail . map f map f . concat = concat . map (map f)
head
、tail
、concat
は完全にポリモーフィックであるのが特徴。list
(concat
の場合はlist
のlist
)を受け取り、順番や要素数を変えたり要素を摘出したりする。が、実際の要素の型やその性質はまったく使われない。
そのような関数を自然変換と呼び、そのような関数を適用する前か後かに別の関数を適用しても結果の同一性が担保される、上記のような法則が存在する。
Filterの一性質とその証明
filter
とmap
をあるリストに適用する場合、適用順を入れ替えても等価性が担保される以下の法則が成り立つ:
filter p . map f = map f . filter (p . f)
その証明:
filter p . map f = {filterの第二の定義から} concat . map (test p) . map f = {mapのfunctor法則} concat . map (test p . f) = {test p xの定義から} concat . map (map f . test (p . f)) = {mapのfunctor法則} concat . map (map f) . map (test (p . f)) = {concatの自然変換性} map f . concat . map (test (p . f)) = {filterの第二の定義から} map f . filter (p . f)
同一性を担保する法則を使ってexpressionを変換していくことでプログラムの性質を証明していくのがThinking Functionally with Haskellの主眼で、これがその第一例。また、Functor(関手)、Natural Transformation(自然変換)など圏論的な話もはじめて出てきた。なかなか面白い。これからが楽しみ。