PS

Applicative functor

圏論 Haskell Applicative

記法

$\mathcal{S} := \mathcal{Set} \text{ or } \mathcal{Hask}$

とする。

特に、 $\mathcal{S} = \mathcal{Hask}$ のとき、free theoremを想定すれば、naturalityの要件は自明となる。

Monoidal sets

$\mathcal{S}$ は、productとsingleton setにより、monoidal category:

$( \mathcal{S}, \times, {\tt \lbrace \ast \rbrace})$

を成す。

Monoidal endofunctor over sets

Monoidal endofunctor:

$(F, \phi, u) : ( \mathcal{S}, \times, {\tt \lbrace \ast \rbrace} ) \to ( \mathcal{S}, \times, {\tt \lbrace \ast \rbrace} )$

とは、

endofunctor: $F : \mathcal{S} \to \mathcal{S}$
natural transformation: $(\phi _ {a, b} : Fa \times Fb \to F(a \times b)) _ { a, b }$ 　(multiplication)
$\mathcal{S}$ -object: $u : F ( {\tt \lbrace \ast \rbrace} )$ 　(unit)

で、

$F( (\ast, q) \mapsto q)(u\ \phi\ y) = y$ 　(left unitality)
$F( (p, \ast) \mapsto p)(x\ \phi\ u) = x$ 　(right unitality)
$F( (p, (q, r) ) \mapsto ( (p, q), r))(x\ \phi\ (y\ \phi\ z)) = (x\ \phi\ y)\ \phi\ z$ 　(associativity)

を満たすもの。 $\phi$ のnaturalilty:

$F \big( (p, q) \mapsto (f(p), g(q) ) \big)(x\ \phi\ y) = F(f)(x)\ \phi\ F(g)(y)$

に注意する。

Applicative functor

Control.Applicativeより、applicative functor:

$(F, {\tt pure}, {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}})$

とは、

endofunctor: $F : \mathcal{S} \to \mathcal{S}$
関数族: $( \mathtt{pure} _ a : a \to F a ) _ {a}$
関数族: $( \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}} _ {a, b} : F ( a \to b) \to Fa \to Fb ) _ {a, b}$

で、

$\mathtt{pure}(1 _ a)\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ x = x$ 　(identity)
$\mathtt{pure} ( f )\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ \mathtt{pure}(x) = \mathtt{pure} ( f(x) )$ 　(homomorphism)
$v\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ \mathtt{pure} (x) = \mathtt{pure} (t \mapsto t(x) )\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ v$ 　(interchange)
$\big( ( \mathtt{pure} (s \mapsto t \mapsto s \circ t)\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ x ) \ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ y \big)\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ z = x \ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ (y\ \mathtt{\unicode{x003c} \unicode{x002a} \unicode{x003e}}\ z)$ 　(composition)

および、

$F(f)(x) = {\tt pure} _ {a \to b} (f)\ {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}} _ {a, b}\ x$ *1

を満たすものとする。

命題

Endofunctor:

$F : \mathcal{S} \to \mathcal{S}$

について、

- $\cong \lbrace ({\tt pure}, {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}}) \mid (F, {\tt pure}, {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}}) \text{ is applicative} \rbrace$

証明

- ${\tt pure} _ a (x) := F(\ast \mapsto x)(u)$
- $f\ {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}} _ {a, b}\ x := F( (t, y) \mapsto t(y) )(f\ \phi\ x)$
- $u := {\tt pure} _ { \lbrace \ast \rbrace } (\ast)$
- $x\ \phi _ {a, b} \ y := F(a \mapsto b \mapsto (a, b) )(x)\ {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}} _ { b, a \times b}\ y$

これらの対応は互いにinverse。

(あやしい)系

$( {\tt pure} _ a : a \to F a ) _ {a}$
$( {\tt \unicode{x003c} \unicode{x002a} \unicode{x003e}} _ {a, b} : F ( a \to b) \to Fa \to Fb ) _ {a, b}$

は、free theoremなしでも共にnatural。

参考文献

*1:free theoremを想定する場合、fmapの一意性 - PSより必ず成立する