Why are the laws of an applicative functor defined the way they are?

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?

As described in the original idioms paper, Applicative (called Idiom there) corresponds to a strong lax monoidal functor. This can be formulated as:

class (Functor f) => MFunctor f where
unit :: () -> f ()
pair :: (f a, f b) -> f (a, b)


The applicative functor laws are then equivalent to the above operations being "monoidal" in the following sense (plus the functor laws):

fmap snd (pair (unit (), u)) = u
fmap fst (pair (u, unit ())) = u
fmap (\(a, (b, c)) -> ((a, b), c)) (pair (u, pair (v, w))) = pair (pair (u, v), w)

The "strength" aspect comes from the fact that these operations (and the functor ones) are "first-class". In a language without higher-order functions, the lax monoidal functor would not be strong. (The usual presentation of Applicative doesn't even make sense in a language without higher-order functions whereas the MFunctor presentation does.)

So, dropping any of the laws means you don't have a lax monoidal functor.

Yet another way of looking at it is to note that the applicative functor operations and laws give rise to a family of operations: liftN :: ((a1, ..., aN) -> b) -> (f a1, ..., f aN) -> f b with unit = lift0 id and pair = lift2 id. Using Agda, we could present this more formally as:

open import Level

data List {i : Level}(A : Set i) : Set i where
Nil : List A
Cons : A → List A → List A

record ⊤ : Set where
constructor tt

record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B

All : (Set → Set) → List Set → Set
All P Nil = ⊤
All P (Cons x xs) = P x × All P xs

module _ {F : Set → Set}
(map : {A B : Set} → (A → B) → F A → F B)
(unit : ⊤ → F ⊤)
(pair : {A B : Set} → F A × F B → F (A × B))
where
pull : {As : List Set} → All F As → F (All (λ A → A) As)
pull {Nil} tt = unit tt
pull {Cons A As} (x , xs) = pair (x , pull {As} xs)

liftN : {B : Set}{As : List Set} → (All (λ A → A) As → B) → All F As → F B
liftN f xs = map f (pull xs)


This perspective arises due to the connection between monoidal categories and multicategories. A lax monoidal functor corresponds to a map of multicategories, liftN being the action on multiarrows. If Haskell had multi-ary functions, it would be natural to model it with a multicategory. The appropriate analogue of "functor" would be a map of multicategories, i.e. an applicative functor. From the multicategory perspective, the applicative functor laws are what make the action on multicomposition coherent. Roughly speaking, if we dropped, say, the associative law for pair, this would be akin to having functions with a binary tree of parameters instead of a list of parameters. One could explore generalized multicategories for this.

StackExchange Computer Science Q#79894, answer score: 9