8
$\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$
1

2 Answers 2

9
$\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$
4
  • $\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$ Commented Aug 10, 2017 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$ Commented Aug 10, 2017 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$ Commented Aug 11, 2017 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$ Commented Aug 14, 2017 at 3:35
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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