40
$\begingroup$

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.

$\endgroup$
35
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Thanks for the answer. Do I understand it correctly that all instances of Functor have a strength (WRT product), simply because they're defined using fmap inside the language? Also, what puzzles me that your definition of $\phi$ and $i$ is reversed compared to both your blog post and the Wikipedia article - is it a typo? I tried to define pure using i as pure' = \v -> fmap (\() -> v) (i ()), which clearly needs i :: (Applicative f) => () -> f (). $\endgroup$ – Petr Pudlák Aug 27 '12 at 11:29
  • 1
    $\begingroup$ I had a typo in this answer -- now fixed. And yes, all instances of Functor are strong (wrt product). $\endgroup$ – Neel Krishnaswami Aug 27 '12 at 11:43
  • $\begingroup$ Could you please also elaborate where Monad stands? If I understand right it's a monoidal endofunctor as well. $\endgroup$ – egdmitry Jun 17 '14 at 17:51
  • $\begingroup$ @egdmitry Monoidal, not monadal. This means the we deal with an endofunctor of a monoidal category (in this case $\operatorname{Hask}$ being monoidal relative to cartesian product, i.e. pairs). $\endgroup$ – kirelagin Sep 2 '16 at 8:54
  • $\begingroup$ May I propose to use the word strengthy to avoid clash of notation with "strong"? It's a Scottish (so particularly spot-on here) dialectal variation of "strong", first used in Wycliffe's Bible. $\endgroup$ – Fosco Oct 17 at 8:46
3
$\begingroup$

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.)

$\endgroup$

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.