Applicative Functor and Monoidal Functor

なんか、Haskell のMonadがApplicative を要求するようになっていて、Monad を作るのが面倒になって困っていたんですが、そもそも、

　　なんで Applicative が必要なのか良くわからない

て問題が。

　　http://learnyouahaskell.com/functors-applicative-functors-and-monoids

とか、まぁ、面白いんだけど、

　　で、それって圏論的にはどうなの?

という疑問が。Functor は、

fmap :: ( a → b ) → f a → f b

で、これが関手の射の写像に対応するってのは、まぁ、わかる。だからなんなのってのは置いといて。

　　pure :: a -> f a
　　<*> :: f (a -> b) -> f a -> f b

こっちはなぁ。fmap の写像が関手、つまりHaskellのデータ構造に包まれてるみたいな感じ。

なのですが、MacLean には Applicative Functor とかなくて。で、

　　https://stackoverflow.com/questions/35013293/what-is-applicative-functor-definition-from-the-category-theory-pov

これによると、圏の積の構造を保存するFunctorである、Monoidal Functor と同じなんだとか書いてある。MacLean だと Monoidal Functor は一章使ってある。それかぁ。面倒くさそうなの避けていたんだけど。

で、Monoidal Functor ってのは、

unit :: f ()
φ :: (f a , f b ) → f ( a , b)

のことだそうです。あぁ、まぁ、積を写像しているような感じ。

** :: f a → f b → f ( a , b )
** x y = φ ( x , y )

としても良いらしい。逆に、

　　　φ ( x , y ) = ** x y

ですね。要するに引数に出てくる積は Curry 化でなくせるというわけ。そういう風に、Monoidal Functor から直積をなくしたのが Applicative Functor ってことね。

実際に、Monoidal functor と Applicative functor の相互変換もできるんですが、ちょっとしたパズルみたいな感じ。Sets だから射とかも集合の要素としてとってこれるので、変換できるらしい。つまり、

　　Sets 以外には Applicative Functor は無意味

な感じらしい。

ついでに Monoidal 圏と Monoidal Functor も Agda で1日で書けたんですが、忙しい時期にそんなことやってていいのか?

この後、Applivative law から Monodail law だすとか、その反対とか、Sets が Monodail 圏なこととか、いろいろやらないといけないようですが、ちょっと量が多い感じだな。


で、結局、Applicative Functor なんの役に立つの? ってことですが、まぁ、あんまり良くはわからないです。データ構造に写像も格納できて便利ってことかな。なんか最初の理解から進んでないぞ。

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/808b03184fd3/monoidal.agda