Haskellの変態的なzipの定義 #haskell

※ ここで挙げるzipの定義はあくまで下記の本に乗っていたものです。実際の定義とは異なります。念のため

foldrの融合則とか言う定理がさらっと出てくるのですが、ググってもあまり情報が出てこないのです。

困っていたら、この間のH本読書会の懇親会で「関数プログラミング入門に説明が載ってるよ」という情報を得て、読んでみることにしました*1。

今回は、そのfoldrの融合則の話ではなくて、zipの定義をfoldrで書いてある部分があったのですが、(´・ω・`)?となったのでネタにしたいと思います。

zipの定義

zip = foldr f e
  where e ys = []
        f x g [] = []
        f x g (y:ys) = (x,y) : g ys

こんな感じの定義なのですが、初見で理解できませんでした。(^^;

zipの型はこんな感じです。

zip :: [a] -> [b] -> [(a,b)]

そして、foldrはこんな感じすね。

foldr :: (a -> b -> b) -> b -> [a] -> b

これにfとeを部分適用しているので、普通に考えれば、zipの型は [a] -> bとなるはず・・・。( ﾟдﾟ)?

型が合ってない。

いやいや、まてよ、whereの部分もなんかおかしい。

e :: a -> [b]
e ys = []

eの型はこういう感じ？

f :: a -> ([b] -> [(a, b)]) -> [b] -> [(a, b)]
f x g [] = []
f x g (y:ys) = (x,y) : g ys

fの型は・・・。(; ﾟдﾟ)ｺﾞｸﾘ

:t foldr f e
foldr f e :: [a] -> [b] -> [(a, b)]

そして、foldr f e の型は・・・・。あれ？zipと同じになってる！？

冷静に考えましょう。

まず、eの型ですが、定義を直訳するとa->[b]になるのですが、引数がわざわざysになっているので、意味的にはリストを撮るということだと思いますので、[a] -> [b]と解釈されるのだと思います。

もっと言うと、xsでなくysとなっているのは、全体の文脈に適用された時に2番目の型だということを表しているっぽいです。

つまり、[b] -> [?]となるハズです。

そして、fの型宣言でそれっぽいものは無いかと適当に当てはめてみると・・・(ここは野生の勘)、?部分が(a,b)というタプルと解釈されると辻褄が合いそうです。

これで、最終的なeの型を手動推論すると、こんな感じになります。

e :: [b] -> [(a,b)]

fの第二引数gの型([b] -> [(a,b)])と一致します！(やったー！)

Haskellの型パラメータ(aとかbの奴)は、単純な型だけじゃなく、関数や関数の引数や戻り値がデータ型(リストやタプルやその他、更にその入れ子)になっている複雑な型を適用することもできるってことですね。

今回はfoldrのb、つまり畳込みをした後の型が([b] -> [(a,b)])になるように調整されていたというわけです。

実際にfoldrの型宣言に当てはめてみましょう。

foldr :: (a -> ([b] -> [(a,b)]) -> ([b] -> [(a,b)])) -> ([b] -> [(a,b)]) -> [a] -> ([b] -> [(a,b)])

ひえー。複雑。(^^;

zipの定義では、foldr f eによって、2つの引数が部分適用されるので・・・。

zip :: [a] -> [b] -> [(a,b)] -- 左結合なのでカッコを外した

おお。zipの型になってる！？( ﾟдﾟ)

Haskellって凄いですね。

この変換を型宣言なしで、さらっとやってのける。そこにシビれる憧れるぅ！

というか、この本、入門書・・・・？

ちなみに冒頭のfoldrの融合則にはまだたどり着いていません。orz

*1:実は、この本買って積んであったのですが、パラパラ見た感じで初心者向けっぽかったので後回しにしてました。読んでみると後半は「入門？」という(^^;