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?
Why are the laws of an applicative functor defined the way they are?
terminology;functional programming;category theory