Let's recall the definition of an applicative functor. Throughout this question, I write $x: T$ to denote that the value $x$ has type $T$.
Definition: An applicative functor consists of a type constructor $F: * \to *$ together with two operations:
- a function $\mathsf{pure}: A \to F(A)$ that transforms a base value $x: A$ into a "wrapped" value $\mathsf{pure}(x): F(A)$.
- a binary operation $\circledast: F(A \to B) \to F(A) \to F(B)$ that applies a wrapped function $f: F(A \to B)$ to a wrapped value $x: F(A)$ and produces a wrapped result $f \circledast x: F(B)$.
We require these operations to satisfy the following conditions:
Wrapped identities apply as identities. $$ \mathsf{pure}(\operatorname{id}) \circledast x = x $$
Wrapped composition applies as composition. $$ \mathsf{pure}(\circ) \circledast f \circledast g \circledast x = f \circledast g \circledast x $$ Here, $\circ$ denotes the function composition operator.
Wrapping distributes across function application. $$ \mathsf{pure}(f(x)) = \mathsf{pure}(f) \circledast \mathsf{pure}(x) $$
Wrapping exchanges across application. $$ f \circledast \mathsf{pure}(x) = \mathsf{pure}(g \mapsto g(x)) \circledast f $$
Question: Why are these the "correct" laws for an applicative functor? To be more precise,
- Are these laws known to be logically independent, in the sense that none of these four laws can be derived from the other three?
- Assuming the answer to question 1 is "yes," what essential characteristic of applicative functors would be lost if we dropped each law, in turn, from the definition? In other words, for each law $L$, there should exist structures $(F, \mathsf{pure}, \circledast)$ satisfying all laws except $L$; why do we not want to call these applicative functors?