PS

fmapの一意性

圏論命題 Functor Haskell

命題

Functor:

$F : \mathcal{Hask} \rightarrow \mathcal{Hask}$

について、

$F'(1 _ a) = 1 _ {F a}$

を満たす関数族:

$( F' _ {a, b} : (a \rightarrow b) \rightarrow Fa \rightarrow Fb ) _ {a, b}$

が存在するならば、

$F(f) = F'(f)$

証明

Free theoremにより、 $F' _ {a, b}$ は、 $b$ についてfreely naturalなので

$F'(f \circ 1) = F(f) \circ F(1) = F(f)$

vs. Applicative

\f -> \x -> pure f <*> x

は、functorialなので、上記の命題より

fmap f x = pure f <*> x

参考文献