Explaining Applicative functor in categorical terms - monoidal functors

Question

I'd like to understand Applicative in terms of category theory.

The documentation for Applicative says that it's a strong lax monoidal functor.

First, Wikipedia page about monoidal functors says that a monoidal functor is either lax or strong. So it seems to me that either one of the sources is wrong, or they use the terms differently. Can anybody explain that?

Second, what are the monoidal categories of which Applicative are monoidal functors? I assume that the functors are endo-functors on the standard Haskell category (objects = types, morphisms = functions), but I have no idea what is the monoidal structure on this category.

Thanks for help.

Answer 1

There are actually two uses of the word "strength" in play here.

• A strong endofunctor $F : C \to C$ over a monoidal category $(C, \otimes, I)$ is one which comes with a natural transformation $\sigma : A \otimes F(B) \to F(A \otimes B)$, satisfying some coherence conditions with respect to the associator which I will gloss over. This condition is sometimes also pronounced "$F$ has a strength".

• A lax monoidal functor $F : C \to D$ is a functor between two monoidal categories $(C, \otimes, I)$ and $(D, \oplus, J)$ with natural transformations $\phi : F(A) \oplus F(B) \to F(A \otimes B)$ and $i : J \to F(I)$, again satisfying a coherence condition with respect to the associators.

• A strong monoidal functor $F : C \to D$ is one in which $\phi$ and $i$ are natural isomorphisms. That is, $F(A \otimes B) \simeq F(A) \oplus F(B)$, with $\phi$ and its inverse describing the isomorphism.

An applicative functor, in the sense of Haskell programs, is a lax monoidal endofunctor with a strength, with the monoidal structure in question being the Cartesian products. So this is why you get the paradoxical-sounding term "strong lax monoidal functor".

As an aside, in a Cartesian closed category, $F$ having a strength is equivalent to the existence of a natural transformation $\mathrm{map} : (A \Rightarrow B) \to (F(A) \Rightarrow F(B))$. That is, having a strength means that the functorial action is definable as a higher-order function in the programming language.

Finally, if you're interested in the type theory of Haskell-style applicative functors, I've just blogged about it.

Answer 2

To understand Applicative, as induced by a monad, I want to point out the following construction:

The Yoneda lemma implies that there is an isomorphism between $FA$ and $\mathrm{nat}(\mathrm{Hom}(A,B),FB)$. In the category of Haskell types, this is the mapping $$a\mapsto\left(g\mapsto F(g)(a)\right)$$ of type $$FA\to B^A\to FB.$$ Evaluating at $FA$, then applying the functors arrow map to the resulting function - if the components of the natural transformation make sense as arrows - and abstracting $FA$ again, we obtain a mapping of type $$FA\to F\,B^A\to FFB.$$ Now if the functor comes with a monadic 'join', mapping from $FFB$ to $FB$, and if we switch around the lambda abstractions and thus the first two argument slots, we can we can obtain a function of type $$F\,B^A\to FA\to FB,$$ which one denotes by <*>. (This is also what you get via $\mathrm{LiftM2\ id}$ in Haskell.)