Arantium Maestum

プログラミング、囲碁、読書の話題

Thinking Functionally with Haskell勉強メモ: 第4章2 concat/map/filter、functorと自然変換、同一性の証明

リストに対する処理の性質・法則、Functorに対するの一般化、性質の証明法についてメモ:

まずはconcatmapfilterの定義:

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という。maplistに対して上記二点の性質を持つが、そのような性質を保つmapに似た関数が定義されている他のデータ構造もありえる。

そのようなデータ構造の型クラスとしてFunctorが用意されている:

class Functor a where
  fmap :: (b -> c) -> a b -> a c

listの場合a ba c[b][c]に置き換えられて、fmap :: (b -> c) -> [b] -> [c]mapの型に合致する。

fmapmapの二つの性質をFunctor type classのInstanceに対して持つ(というかmaplistに対する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)

headtailconcatは完全にポリモーフィックであるのが特徴。listconcatの場合はlistlist)を受け取り、順番や要素数を変えたり要素を摘出したりする。が、実際の要素の型やその性質はまったく使われない。

そのような関数を自然変換と呼び、そのような関数を適用する前か後かに別の関数を適用しても結果の同一性が担保される、上記のような法則が存在する。

Filterの一性質とその証明

filtermapをあるリストに適用する場合、適用順を入れ替えても等価性が担保される以下の法則が成り立つ:

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(自然変換)など圏論的な話もはじめて出てきた。なかなか面白い。これからが楽しみ。