PS

Traversable functor

圏論定義 Haskell Traversable

記法

$\mathcal{App} :=$ Category of applicative functors - PS
$\mathcal{S} := \mathcal{Set} \text{ or } \mathcal{Hask}$

Traversable functor その1

functor: $T : \mathcal{S} \to \mathcal{S}$
natural transformation: $( \mathtt{sequenceA} ^ F : T F \Rightarrow F T ) _ { F \in \mathcal{App} }$ *1

のペアで

$\mathtt{sequenceA} ^ {1 _ \mathcal{S}} = 1 _ T$ 　(unitality)
$F\ \mathtt{sequenceA} ^ G \circ \mathtt{sequenceA} ^ F\ G = \mathtt{sequenceA} ^ {FG}$ 　(linearity)

を満たすもの。

Traversable functor その2

functor: $T : \mathcal{S} \to \mathcal{S}$
natural transformation: $\big( (\mathtt{traverse} ^ F _ {a, b} : (a \to F b) \to T a \to F T b) _ {a, b} \big) _ { F \in \mathcal{App} }$ *2

のペアで

$\mathtt{traverse} ^ {1 _ \mathcal{S}} _ {a, b}(f : a \to b) = T(f)$ 　(identity)
$F(\mathtt{traverse} ^ G _ {b, c} (g : b \to Gc)) \circ \mathtt{traverse} ^ F _ {a, b} (f : a \to Fb) = \mathtt{traverse} ^ {F G} _ {a, c} ( F(g) \circ f)$ 　(composition)

を満たすもの。Free theoremを想定する場合、(identity)は、fmapの一意性 - PSにより

$\mathtt{traverse} ^ {1 _ \mathcal{S}} _ {a, a} (1 _ a) = 1 _ {T a}$

で十分(と思う)。

命題

その1とその2は同値。具体的には

$\mathtt{sequenceA} ^ F \mapsto \big( (f : a \to Fb) \mapsto \mathtt{sequenceA} ^ F _ b \circ T(f) \big) _ {a, b}$
$\mathtt{traverse} ^ F \mapsto ( \mathtt{traverse} ^ F _ {Fa, a} (1 _ {F a})) _ a$

の対応は互いにinverse。

参考文献

*1:各componentもnatural transformation

*2:各componentもnatural transformationでないといけない(と思う)