Haskell

Data.Foldableの正体

リストにおいて foldr は最も基本的な関数と言えるでしょう。例えば関数型プログラミングでは欠かせないmapfilterといった関数は

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

map f = foldr (\a bs -> f a : bs) []

filter :: (a -> Bool) -> [a] -> [a]
filter p = foldr (\a as -> if p a then a : as else as) []

というようにfoldrを使って実装することができます。

この foldr をリストだけではなく他のデータ構造にも一般化しようという試みの一つにRecursion Schemesがあります。Recursion Schemesの一つであるCatamorphismはF始代数から伸びる唯一の射であり、特に foldr

data ListF a r = Nil | Cons a r

deriving Functor

というような Functor ListF の Catamorphism とみなすことができます1

もう一つ、foldrを一般化する方法としてHaskellの標準ライブラリであるbaseに実装されている型クラスFoldableがあります。

class Foldable t where

{-# MINIMAL foldMap | foldr #-}

foldMap :: Monoid m => (a -> m) -> t a -> m
foldMap f = foldr (mappend . f) mempty

foldr :: (a -> b -> b) -> b -> t a -> b
foldr f z t = appEndo (foldMap (Endo . f) t) z

{-# MINIMAL foldMap | foldr #-}foldMap2 もしくは foldr のいずれかを定義すれば Foldable のインスタンスを作ることが出来るということを示すためのプラグマです。つまり Foldable はデータ型ごとにアドホックな foldr を定義できるようにした一般化といえるでしょう。

僕は今まで Foldable に関して2つの疑問を抱いていました。1つは Foldable のインスタンスは foldr ではなく foldMap を実装することで定義することが出来るが3、こっちは型に Monoid の制約が現れていて気持ち悪い。もう一つはCatamorphismも Data.Foldablefoldr の一般化ですが両者はどういう関係なのか。特にRecursion Schemesがある関手の始代数・終余代数と特徴づけられる一方でData.Foldableに数学的な背景が存在するのか。


Data.Foldableの正体に迫る

Data.Foldableについて歴史的な背景を探ろうとしましたがGHCのコミット履歴を見てもFoldableがどこから来たのかを示す記録はありませんでした4。しかし以下の記事を見つけて僕の疑問が一気に解決しました。

The Comonad.Reader » Free Monoids in Haskell

曰く


  • Haskellにおいてリストは厳密には自由モノイドではない

  • Haskellでは等式制約や商集合を扱うことができないので自由モノイドを実装することはできない

  • しかしもし a の自由モノイド FM a が存在すれば任意のモノイド m への埋め込み a -> m に対してモノイド準同型 FM a -> m が存在するということをモデル化することができる


  • Foldable の最も基本的な関数は toFreeMonoid

3つ目の条件は FM に対して

forall m. Monoid m => (a -> m) -> FM a -> m

という型の関数を定義することでモデル化することができるということです。

ここで手元のAwodey(赤青色の圏論の本ですね)をめくってみると数学的な自由モノイドの定義は

集合 $A$ が与えられた時に$M(A)$ が $A$ の自由モノイドであるとは、 $A$ から $M(A)$ の台集合5 $|M(A)|$ への写像 $i : A \rightarrow |M(A)|$ が存在して、任意のモノイド $N$ と $A$ から $N$ の台集合 $|N|$ への写像 $f : A \rightarrow |N|$ が与えられた時に、 $M(A)$ から $N$ へのモノイド準同型 ${\bar f}$ が唯一つ存在して、その台集合上の写像 $\left|{\bar f}\right|$ に対して $\left|{\bar f}\right| \circ i = f$ が成り立つようなものである。

と大体書いてあります。つまり(ざっくりいうと)集合 $A$ から任意のモノイド $N$ への写像 $f$ が与えられた時に、 $A$ の自由モノイド $M(A)$ から $N$ へのモノイド準同型で以下の可換図式を可換にするようなもの $|{\bar f}|$ が唯一つ存在するということです。

この性質をHaskellの関数(の型)として書き下すと

forall m. (a -> m) -> FM a -> m

となります。ここで FMa の自由モノイドを対応付ける関手(Functor)と考えることができます。この型は

forall m. FM a -> (a -> m) -> m

と同型であり、ここから

newtype FM a = FM { unFM :: forall m. Monoid m => (a -> m) -> m }

というように FM の型の定義を考えることができます(ちなみにunFMの型が forall m. FM a -> (a -> m) -> m となります)。この FM a が自由モノイドであることを確かめるために a から FM a への関数 embed 6Monoid のインスタンスを定義してみましょう。

embed :: a -> FM a

embed x = FM $ \k -> k x

instance Monoid (FM a) where
mempty = FM $ \_ -> mempty
mappend (FM e1) (FM e2) = FM $ \k -> e1 k <> e2 k

以上より FM a $\cong$ Monoid m => (a -> m) -> ma の自由モノイドの型であることが大体分かりました。(2019/04/21追記: コメントいただいたように自由モノイドであることを主張するためにはモノイドであることを確かめるだけでは不十分でflip unFM fの唯一性を証明する必要があります。)

さて Data.Foldable に戻りましょう。 foldMap の型は

foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m

であり、引数の順番を入れ替えると、

foldMap :: (Foldable t, Monoid m) => t a -> (a -> m) -> m

これはまさにFoldableのインスタンスから自由モノイドに変換する関数に他なりません。つまりFoldableとは自由モノイドに変換できるような型のことだったのです7


まとめ

僕がFoldableに対して抱いていた疑問は解決しました。今となっては foldr よりもむしろ Monoid 制約のついた foldMap のほうが Foldable にとって本質的な関数に見えます。そしてFoldableは自由モノイドへの自然変換を備えた関手であるという数学的な見方もできるようになりました3。これで明日から自身を持って Foldable に向き合えるようになり、夜もぐっすりと眠れるようになりそうです :relaxed:


追記: 2019/04/18

Haskell-jpのSlackで @kazu_yamamoto さんより、 Programming in Haskell 2nd Edition にFoldableの起源についての言及が載っていると教えていただきました。どうやら"Calculate Polytypically!"という論文の Crush と呼ばれるものが Foldableの原型となっているようです。さらに読んでみると"9 Crush compared to cata"という章があり、Catamorphismとの関係が議論されていました。ただどうもFoldableの抽象化はGeneric Programmingに近いものでCatamorphismとの関係はあまり無さそうです。





  1. http://hackage.haskell.org/package/recursion-schemes-5.1.2/docs/Data-Functor-Foldable.html#t:ListF 



  2. foldMap についてはこちらが分かりやすいです。 圏論勉強会第2回@ワークスアプリケーションズ#プログラミングにおけるモノイド 



  3. foldrfoldMap の関係についてはこちらが分かりやすいです。 FoldableクラスがfoldMapからfoldrを構成する流れ 



  4. Data.Foldableがどこからどういう経緯でGHCに取り込まれたのか知ってる人がいたら教えてください :pray: 



  5. モノイド $M$ の台集合 $|M|$ とは $M$ から単純にモノイドの構造を忘れ去った集合です。なので演算が忘れられただけで要素は元のモノイドと等しい集合になります。 



  6. 元々 $i : A \rightarrow |M(A)|$ と書いてたやつです 



  7. つまりFoldableとは自由モノイドを与える関手への自然変換を備えた関手のことだったのです8。 



  8. 追記: 2019/4/22 あれ、でも FoldableFunctor を要請していないので自由モノイドに変換できる型という理解が正しいですね。 toFreeMonoid を備えた型ということで。