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.
- 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).
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" ? -
- Applicative Programming with Effects
- hackage: Control.Applicative
- nlab: Monoidal Functor
- Introduction to Coalgebra, Bart Jacobs
- in part 5, it explains strong functor, distributive law
- 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.
- Strong categorical datatypes
- Desugaring Haskell’s do-notation Into Applicative Operations
- Introduction to Higher-Order Categorical Logic