Applicative functor
記法
とする。
特に、 のとき、free theoremを想定すれば、naturalityの要件は自明となる。
Monoidal sets
は、productとsingleton setにより、monoidal category:
を成す。
Monoidal endofunctor over sets
Monoidal endofunctor:
とは、
- endofunctor:
- natural transformation: (multiplication)
- -object: (unit)
で、
- (left unitality)
- (right unitality)
- (associativity)
を満たすもの。 のnaturalilty:
に注意する。
Applicative functor
Control.Applicativeより、applicative functor:
とは、
- endofunctor:
- 関数族:
- 関数族:
で、
- (identity)
- (homomorphism)
- (interchange)
- (composition)
および、
を満たすものとする。
命題
Endofunctor:
について、
証明
これらの対応は互いにinverse。
(あやしい)系
は、free theoremなしでも共にnatural。
参考文献
- Applicative Programming with Effects
- Constructing Applicative Functors
- Monoidal functor - Wikipedia, the free encyclopedia
- monoidal functor in nLab
- lo.logic - Explaining Applicative functor in categorical terms - monoidal functors - Theoretical Computer Science Stack Exchange
- haskell - What exactly are the categories that are being mapped by Applicative Functors? - Stack Overflow
- Applicative functors : Inside 206-105
*1:free theoremを想定する場合、fmapの一意性 - PSより必ず成立する