top page > computer > haskell > web_lecture > for_programmer > concatMap_prop.html
更新日:
文責: 重城良国

関数concatMapの性質

(工事中 0%)

メモ

あとでリストがモノイダル則(を通してアプリカティブ則)を満たすことを示すために、リスト内包表記でできる変形の説明をする。そのためにconcatMapの満たす性質を示しておく必要がある。また、ここで関数concatMapの性質を説明しておくと、モナドの説明のときにすこし入りやすくなるかも。

ここまで、かっちりとやる必要があるかどうかは不明だが、かために使っておいてやわらかくするほうが簡単なので。

[ exp | exp1, (x, y) <- [ (x, y) | x <- xs, y <-ys ], exp2 ]
<=> [ exp | exp1, x <- xs, y <- ys, exp2 ]

を示せるレベルまで。まずは、アトランダムに必要そうな性質を示していこう。あとで整理する。

concatMapについてほぼファンクター、アプリカティブファンクター、モナドの説明のレベルまでしてしまおう。それを何となく覚えていることで本番の説明が入りやすくなるだろう。

流れ

まずはモナド則の変形をconcatMapについて定義する。リスト内包表記の満たす性質を説明する。リスト版のアプリカティブを定義する。リスト版のモノイダル則を説明する。

はじめに

concatMapにはいろいろな性質がある。リスト内包表記をより単純な形に変形するのときにそろ性質を使うことができる。ここでそれらの性質について示す。

演算子(++)の性質

これは定義から明らかだが演算子(++)には以下のような性質がある。

(x : xs) ++ ys == x : (xs ++ ys)

concatMapの定義

ここでは関数concatMapが以下のように定義されているものとする。

concatMap f (x : xs) = f x ++ concatMap f xs
concatMap _ _ = []

分配則

concatMap f (xs ++ ys) == concatMap f xs ++ concatMap f ys

証明

xs = []のときは定義から明らかである。ここでconcatMap f (is ++ ys) == concatMap f is ++ concatMap f ysが成り立つとする。

concatMap f ((i : is) ++ ys)
=> concatMap f (i : (is ++ ys))
=> f i ++ concatMap (is ++ ys)
=> f i ++ concatMap f is ++ concatMap f ys
=> concatMap f (i : is) ++ concatMap f ys

xs = isで成り立つときにxs = i : isで成り立つことが証明された。数学的帰納法によりconcatMap f (xs ++ ys) == concatMap f xs ++ concatMap f ysは任意のxsで成り立つ。

結合則

concatMap (concatMap f . g) == concatMap f . concatMap g

「関数concatMapによる関数filterの定義」へもどる 「構文: リスト内包表記1」へ

正当なCSSです! HTML5 Powered with CSS3 / styling, and Semantics