6
$\begingroup$

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?
$\endgroup$
8
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for this awesome answer! But I do have one specific question that I didn't see you or the idioms paper touch on. Nothing you've said actually proves that "dropping any of the laws means you don't have a lax monoidal functor." As I found in a similar question on Math.SE about vector spaces, a reasonable-looking set of laws can carry subtle logical dependencies making some of them redundant. I would specifically like to know if this occurs for the applicative functor laws... $\endgroup$ – David Zhang Aug 10 '17 at 17:55
  • $\begingroup$ ...in particular, the exchange law feels a little contrived, and is not actually necessary to prove e.g. that applicative functors become functors when one defines $\mathsf{fmap}(f,x) := \mathsf{pure}(f) \circledast x$. To conclusively show that no such dependencies exist, it suffices to exhibit structures satisfying each set of three laws but not the fourth, and frankly, I'm having trouble conceiving of such a structure for any set of three. $\endgroup$ – David Zhang Aug 10 '17 at 18:00
  • 2
    $\begingroup$ This is a somewhat context-dependent question. Do you want to know if this is the case mathematically, only in the strong context, or only for Haskell? How much are you willing to idealize Haskell if the last? It is almost certain that some of these laws are redundant if we consider free theorems from parametricity and ignore the strictness side-conditions on them. The first two laws you mention are closely related to the Functor laws, and so, for example, the first law likely implies the second modulo strictness. $\endgroup$ – Derek Elkins Aug 11 '17 at 0:36
  • $\begingroup$ Hmm, that's a good point I hadn't considered. I was originally interested in the strict sub-language of Haskell, so I guess I'll need to venture into the world of bottoms to find the examples I seek. By the way, what do you mean by "the strong context"? $\endgroup$ – David Zhang Aug 14 '17 at 3:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.