Applicative Functor (a.k.a. Strong Lax Monoidal Functor) [DRAFT]

Created at 2016-05-05T04:13:43.000Z
### Summery

Motivation

Use case:

Theoretical exposition:

The most important line:

pure function applied to funny arguments

Compositionality of

*Applicative Functor*comes from Compositionality of*strong lax monoidal functor*.I don't know how to deal with usual

*functor*for additional type constructor in language.

### Notes

- Original motivation for giving semantics to effectful computation by _Monad_ is:
- equational reasoning

- But, by removing monadic equation constraint, what _Applicative_ does is to give semantics to effectful computation which could bring:
- faster effect resolution (e.g. reader, parallel computation,
*Traversable*), - "practically interesting" effect resolution (e.g. matrix transposition).

- faster effect resolution (e.g. reader, parallel computation,
I don't feel "more than one free variable" is not the point of strength required for applicative...

In Haskell (or in $Sets$), any

*Functor*is*strong*. So, I think*strong*-ness shouldn't be emphasized in this discussion, it's confusing.- What kind of "formal language" are we talking about for _Applicative_ computation?
- it will be "language without
*let*(a.k.a binding)" - what's the crucial difference of "join" and "crushing effect (traverse effect along data structure)"?
- traverse doesn't require "binding" ? -

- it will be "language without

### References

- Applicative Programming with Effects
- hackage: Control.Applicative
- nlab: Monoidal Functor
- Introduction to Coalgebra, Bart Jacobs
- in part 5, it explains
*strong functor*,*distributive law*

- in part 5, it explains
- Notions of Computation and Monads, E. Moggi
- in 3rd section, it explains that
*strong monad*is necessary to give semantics for the language which accommodates more than one free variable.

- in 3rd section, it explains that
- Strong categorical datatypes
- Desugaring Haskellâ€™s do-notation Into Applicative Operations
- Introduction to Higher-Order Categorical Logic