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

Question

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,

1. Are these laws known to be logically independent, in the sense that none of these four laws can be derived from the other three?
2. 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?

Answer 1

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.

Answer 2

There is an answer to your question from the viewpoint of practical functional programming. Applicative functors are then defined via the zip method, not via ap. The zip method is clearly a useful method in practice, and a programmer with some practical experience expects zip to have certain properties. One of these properties is the associativity law:

  fa `zip` (fb `zip` fc) should return a value of type F (A, (B, C))
  (fa `zip` fb) `zip` fc should return a value of type F ((A, B), C)
  These two values should be equal after flattening the tuples via F's fmap

Similarly one can formulate other properties of zip and pure from the programmer's perspective. If those properties don't hold, programs using zip will be much harder to write correctly, because the order of zipping will affect the results, etc.

After that, you can show that zip and pure is equivalent to ap. It is not easy to just derive the laws of ap from the laws of zip, the types get quite complicated. So, instead, we can motivate the laws of ap directly from formal considerations of category theory. We consider ap's type signature:

 ap :: F (a -> b) -> F a -> F b

This looks like a lifting from one sort of functions (of type F(a -> b)) into another sort of functions (of type F a -> F b). It is natural to require that this kind of lifting should satisfy identity and associativity laws. Then you just need to write those laws and complete the proofs.

This is the approach I am using in Chapter 9 of my book "The Science of Functional Programming". LyX/LaTeX source: https://github.com/winitzki/sofp pdf: https://leanpub.com/sofp That book is written with programming examples in Scala but the material is largely independent of Scala. I show the motivations and full step-by-step proofs of all laws.