関数型言語におけるTraversableとは何か？Functorと比較しながら解説する

#はじめに
Haskellなどの関数型言語にはFunctorやTraversableなどのinstanceが定義されています。
本記事ではこのTraversableに関して、Functorと比較しながらその公理系の意味を解説していきます。

(インライン表示の数式が勝手に改行され、読みづらい場合がありますが、ご了承願います。)

#FunctorとTraversableの定義

まず、FunctorとTraversableの定義を確認します。

Typeを型の集合とし、型変換子T:Type -> Typeとします。

##Functor

型変換子$T$に対して、以下を満たす演算$\operatorname{fmap}_T : \forall A,B, (A \to B) \to T,A \to T,B$が存在する場合、
$\operatorname{fmap}_T$がTにおけるFunctorであるといい、Functorが存在するような型変換子Tのことを単にFunctorと呼ぶ。

\forall A, \operatorname{fmap}_T \operatorname{id}_A = \operatorname{id}_{(T\,A)}

\forall A\,B\,C, \forall f:B \to C,\forall g:A \to B,\, \operatorname{fmap}_T (f \circ g) = \operatorname{fmap}_T f \circ \operatorname{fmap}_T g

##Traversable
本記事では、Functorであるような型変換子$T$に対し、以下を満たす
$\operatorname{traverse}_T: \forall M : \operatorname{Applicative},,\forall A,B, (A \to M,B) \to T,A \to M,(T,B)$が存在する場合、
型変換子TがTraversableであると定義します。¹

\forall A, \operatorname{traverse}_{T,\operatorname{id}}\operatorname{id}_A = \operatorname{id}_{(T\,A)}

\forall M\,N, \forall A\,B\,C, \forall f:B \to N\,C,
\forall g:A \to M\,B,\\
\operatorname{traverse}_{T,(M \circ N)} (\operatorname{fmap}_M f \circ g) = \operatorname{fmap}_M (\operatorname{traverse}_{T,N} f) \circ \operatorname{traverse}_{T,M} g

ここで、Traversableの公理にはMの演算として$\operatorname{fmap}_M$しか現れないので、MはApplicativeではなくFunctorでも良さそうに見えますが、
具体的にMaybeなどのTraversable性を示すのには$\eta : \forall A, A \to M,A$,
Listなどの多引数コンストラクタを含む型変換子のTraversable性を示すのには$<*> : \forall A,B, M,(A \to B) \to M,A \to M,B$が必要になるため、FunctorではなくApplicativeで定義しています。

###HaskellにおけるTraversable

Haskellでは、Traversableは以下のように定義されています。

Data.Traversable.hs

class (Functor t, Foldable t) => Traversable t where
  traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
  -- 以下省略

演算の定義自体はFoldableを継承しているだけで基本的には本記事のものと同じですが、公理が少し異なります。
まず、元の2つの公理に関しては、恒等写像idをコンストラクタIdで記述し、合成写像m . nはコンストラクタComposeを用いて記述されています。

さらに追加でもう一つ公理がありますが、これについて、HaskellのBasic librariesには、「任意のapplicative transformation t :: (Applicative f, Applicative g) => f a -> g aに対し、t . traverse f = traverse (t . f)を満たす」と書いてありますが、この表記だと数学的には以下のような恒真な命題を表すことになってしまうため、厳密には間違いです。

\forall t : \forall M\,N : \operatorname{Applicative}, \forall A, M\,A \to N\,A,\\
 (\forall M\,N, \forall A, \forall x:A, t_{M,N}\,(\eta_M x)= \eta_N x) \to\\
(\forall M\,N, \forall A\,B, \forall f:A \to B, \forall x:M\,A, t_{M,N}\,(f <*>_M x) = (t_{M,N}\,f) <*>_N (t_{M,N}\,x)) \to\\
\forall M\,N, \forall A\,B, \forall f:A \to M\,B, t_{M,N} \circ \operatorname{traverse}_{T,M} f = \operatorname{traverse}_{T,N} (t_{M,N} \circ f)

なぜ恒真になってしまうかというと、Applicative transformationtの型が$\forall M,N : \operatorname{Applicative}, \forall A, M,A \to N,A$であり、特にMとNがここで量化されているからです。

これはCurry-Howard同型対応により、tを与えることは、同じ命題$\forall M,N : \operatorname{Applicative}, \forall A, M,A \to N,A$の証明を与えることと同等になりますが、

M := \lambda X.(X + 1)\\
N := \operatorname{id}\\
A := \emptyset

を与えると偽になるので、このようなtは存在せず、結果的に元の命題がトートロジーであることが言えます。

本当は公理として与える命題は以下のようになるはずです。

\forall M\,N : \operatorname{Applicative},\\
\forall t : \forall A, M\,A \to N\,A,\\
 (\forall A, \forall x:A, t\,(\eta_M x)= \eta_N x) \to\\
(\forall A\,B, \forall f:A \to B, \forall x:M\,A, t\,(f <*>_M x) = (t\,f) <*>_N (t\,x)) \to\\
\forall A\,B, \forall f:A \to M\,B, t \circ \operatorname{traverse}_{T,M} f = \operatorname{traverse}_{T,N} (t \circ f)

このように、MとNを外で量化し、固定されたMとNに対してtがApplicative transformationの公理を満たすときに等式を満たすと定義する必要があります。(HaskellのBasic librariesが参照している元の論文でもこちらの意味を表しています。)

ちなみにこれを仮定すると、

\forall M : \operatorname{Applicative}, \forall A, \forall x:T\,A, \operatorname{traverse}_{T,M} \eta_M\,x = \eta_M\,x

を満たし、1つ目の公理

\forall A, \operatorname{traverse}_{T,\operatorname{id}} \operatorname{id}_A = \operatorname{id}_{(T\,A)}

を一般化できます。

このように、HaskellにおけるTraversableは本記事で定義したTraversableよりも限定された、小さい公理系になっています。

#TraversableとFunctorを比較する

TraversableとFunctorを比較すると、その類似性が見えてきます。

まず、以下のような演算子$<\circ>$を定義します。

<\circ> : \forall M\,N : \operatorname{Functor},\,\forall A\,B\,C, (B \to M\,C) \to (A \to N\,B) \to A \to M\,(N\,B)\\
f <\circ>_{M,N} g := \operatorname{fmap}_N\,f \circ g

すると、traversableの2つ目の公理を以下のように書き換えることができます。

\forall M\,N, \forall A\,B\,C, \forall f:B \to N\,C,
\forall g:A \to M\,B,\\
\operatorname{traverse}_{T,(M \circ N)} (f <\circ> g) = \operatorname{traverse}_{T,N} f <\circ> \operatorname{traverse}_{T,M} g

これはまさに$<\circ>$に対する準同型性を表しており、さらに$M = N =\operatorname{id}$のとき、$<\circ>$の型は$\circ$と一致します。

すなわち、任意の型変換子$T$に対し、

\operatorname{fmap}_T' := \operatorname{traverse}_{T,\operatorname{id}}

と定義すれば、Traversableのもう一つの公理から$\operatorname{fmap}_T'$がTにおけるFunctorになることが言えます。

したがって、$\operatorname{traverse}$とは$\operatorname{fmap}$に対する演算$\circ$を演算$<\circ>$に変えた時の一般化であると言えます。

つまり、本記事で定義したTraversableはまさにFunctorの一般化そのものを表しており、
HaskellにおけるTraversableはFunctorを一般化した公理系にさらに公理を追加したものだと説明できます。

#まとめ

Traversableの公理系について、Functorと比較しながら解説しました。
結果として、TraversableにおけるtraverseとはFunctorにおけるfmapに対する演算$\circ$を演算$<\circ>$に変えた時の一般化であることが分かりました。

1. Applicativeの公理系は「関数型言語におけるMonadクラスはApplicativeを継承するべきなのか？MonadとApplicativeとの関係を再確認する」に記載しています。 ↩