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

<p>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 &lt;*>. 
(This is also what you get via $\mathrm{LiftM2\ id}$ in Haskell.)</p>

CC BY-SA 3.0
2014-08-28T17:41:28.570Z
2015-10-29T12:49:46.423Z
2015-10-29T12:49:46.423Z
Nikolaj-K
<p>There are actually two uses of the word "strength" in play here. </p>

<ul>
<li><p>A <em>strong endofunctor</em> $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".</p></li>
<li><p>A <em>lax monoidal functor</em> $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. </p></li>
<li><p>A <em>strong monoidal functor</em> $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. </p></li>
</ul>

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

<p>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. </p>

<p>Finally, if you're interested in the type theory of Haskell-style applicative functors, <a href="http://semantic-domain.blogspot.com/2012/08/a-computational-lambda-calculus-for.html">I've just blogged about it.</a> </p>

CC BY-SA 3.0
2012-08-27T11:29:59.400Z
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](https://en.wikipedia.org/wiki/Monoidal_functor#Definition) - is it a typo? I tried to define `pure` using `i` as `pure' = \v -> fmap (\() -> v) (i ())`, which clearly needs `i :: (Applicative f) => () -> f ()`.
Petr
CC BY-SA 3.0
2012-08-27T11:43:43.073Z
I had a typo in this answer -- now fixed. And yes, all instances of `Functor` are strong (wrt product).
Neel Krishnaswami
CC BY-SA 3.0
2014-06-17T17:51:52.557Z
Could you please also elaborate where Monad stands? If I understand right it's a monoidal endofunctor as well.
egdmitry
CC BY-SA 3.0
2016-09-02T08:54:39.803Z
@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).
kirelagin
CC BY-SA 4.0
2019-10-17T08:46:03.790Z
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.
fosco
CC BY-SA 3.0
2012-08-27T08:25:24.307Z
2012-08-27T11:41:50.237Z
2012-08-27T11:41:50.237Z
Neel Krishnaswami
<p>I'd like to understand <code>Applicative</code> in terms of category theory.</p>

<p>The <a href="http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Applicative.html">documentation</a> for <code>Applicative</code> says that it's <em>a strong lax monoidal functor</em>.</p>

<p>First, Wikipedia page about <a href="https://en.wikipedia.org/wiki/Monoidal_functor">monoidal functors</a> says that a monoidal functor is either <em>lax</em> or <em>strong</em>. So it seems to me that either one of the sources is wrong, or they use the terms differently. Can anybody explain that?</p>

<p>Second, what are the monoidal categories of which <code>Applicative</code> 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.</p>

<p>Thanks for help.</p>

<lo.logic><type-theory><functional-programming><ct.category-theory>
Explaining Applicative functor in categorical terms - monoidal functors
Petr
# Explaining Applicative functor in categorical terms - monoidal functors

(Asked by: username_0 on 2012-08-27)

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

The [documentation](http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Applicative.html) for `Applicative` says that it's *a strong lax monoidal functor*.

First, Wikipedia page about [monoidal functors](https://en.wikipedia.org/wiki/Monoidal_functor) 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.

**Tags:** lo.logic, type-theory, functional-programming, ct.category-theory

---

## 2 answers

### Answer by username_2 on 2012-08-27. Score: 43 | Accepted answer

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.](http://semantic-domain.blogspot.com/2012/08/a-computational-lambda-calculus-for.html)

> **Comments:**
> **username_0**: 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](https://en.wikipedia.org/wiki/Monoidal_functor#Definition) - is it a typo? I tried to define `pure` using `i` as `pure' = \v -> fmap (\() -> v) (i ())`, which clearly needs `i :: (Applicative f) => () -> f ()`.  
> **username_2**: I had a typo in this answer -- now fixed. And yes, all instances of `Functor` are strong (wrt product).  
> **username_3**: Could you please also elaborate where Monad stands? If I understand right it's a monoidal endofunctor as well.  
> **username_4**: @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).  
> **username_5**: 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.  

---

### Answer by username_1 on 2014-08-28. Score: 4

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


---

