関数型言語における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と呼ぶ。

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

```math
\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である**と定義します。[^1]

[^1]: Applicativeの公理系は「[関数型言語におけるMonadクラスはApplicativeを継承するべきなのか？MonadとApplicativeとの関係を再確認する](https://qiita.com/nekonibox/items/2f89a17e0e7f4dc14961)」に記載しています。

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

```math
\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`は以下のように定義されています。

```haskell: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](https://hackage.haskell.org/package/base-4.16.0.0/docs/Data-Traversable.html)には、「*任意のapplicative transformation `t :: (Applicative f, Applicative g) => f a -> g a`に対し、`t . traverse f = traverse (t . f)`を満たす*」と書いてありますが、この表記だと数学的には以下のような恒真な命題を表すことになってしまうため、厳密には間違いです。

```math
\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 transformation`t`の型が$\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$の証明を与えることと同等になりますが、

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

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


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

```math
\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が参照している[元の論文](http://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf)でもこちらの意味を表しています。)

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

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

を満たし、1つ目の公理

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

を一般化できます。


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


#TraversableとFunctorを比較する

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

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

```math
<\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つ目の公理を以下のように書き換えることができます。

```math
\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$に対し、

```math
\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>$に変えた時の一般化であることが分かりました。