An applicative, in category theory, is a lax monoidal functor with tensorial strength. In the following, we will present the definition as an endofunctor, since the concept has its origin in the context of functional programming where every functor is an endofunctor.
Let be a monoidal category. A lax monoidal endofunctor is a functor together with two coherence maps:
-
(the unit morphism)
such that the following diagrams commute:
\begin{xy} \xymatrix{ (FA\ \otimes\ FB)\ \otimes\ FC \ar[r]^{\alpha} \ar[d]_{\phi_{A,B}\ \otimes\ FC} & FA\ \otimes\ (FB\ \otimes\ FC) \ar[d]^{FA\ \otimes\ \phi_{B,C}} \\ F(A\ \otimes\ B)\ \otimes\ FC \ar[d]_{\phi_{A\ \otimes\ B,C}} & FA\ \otimes\ F(B\ \otimes\ C) \ar[d]^{\phi_{A,B\ \otimes\ C}} \\ F((A\ \otimes\ B)\ \otimes\ C) \ar[r]_{F_{\alpha}} & F(A\ \otimes\ (B\ \otimes\ C)) \\ } \end{xy}The natural transformations:
- (associativity)
- (right identity)
- (left identity)
are part of the monoidal structure on .
Applicative functors are a relatively new concept. They were first introduced in 2008 by Conor McBride and Ross Paterson in their paper Applicative programming with effects.[1] In functional programming where every functor is an endofunctor and every functor applied to the monoidal category , with the tensor product replaced by cartesian product, inherently possesses a unique strength, resulting in every functor within being strong. In simpler terms, a strong lax monoidal functor is just a lax monoidal functor that also has the property of being a strong functor, and its strength coherently associates with the monoidal structure. When we apply this in the context of functors, this coherent association is automatically provided.[2]
Example
The Applicative typeclass in Haskell looks slightly different then our definition of a lax monidal functor. However there is another typeclass in Haskell called Monoidal that reflects our definition. Moreover, there is a equivalence between the two typeclasses Applicative and Monoidal. This parallels our previous demonstration of the interchangeability between bind
and >>=
, as discussed in my post on monads. Let me first introduce the typeclass Monoidal and then we show that this is equivalent to Applicative.
Haskell Definition of Monoidal (Interface)
Please note that fa -> fb -> f(a, b)
is actually the curried version of
(f a, f b) -> f (a, b)
Haskell comes with curry
and uncurry
as part of its standard library, which together form an isomorphism.
Hence we can also phrase Monoidal this way, and it aligns seamlessly with our categorical definition of a strong lax monoidal functor:
We have the usual monoidal laws (pseudocode):
Now that we have established the definition of Monoidal lets have a look at the equivalent Applicative definition in Haskell.
Haskell Definition of Applicative (Interface)
This is how to recover Applicative in terms of Monoidal:
And this is the reverse direction, Monoidal in terms of Applicative:
We’ve now formulated a two-way translation between Applicative and Monoidal, illustrating that they are isomorphic. This equality between Applicative and Monoidal can also be shown in a computer-checked proof in Coq.
Though the compiler does not enforce it, a proper instance of Applicative should comply with the applicative laws:
Now, lets have a look at some instances of Applicative.
An Instance of Applicative, the List Applicative
Another Instance, the Maybe Functor
All of the above is already implemented in the standard Haskell library, so you can also simply open an interactive Haskell interpreter (ghci) and test the following examples.
References
- 0.The diagram displayed at the top of this post is a modified version of Brent Yorgey's Typeclassopedia diagram ↩
- 1.McBride, Conor; Paterson, Ross (2008-01-01). Applicative programming with effects (pdf). Journal of Functional Programming. 18 (1): 1–13. doi:10.1017/S0956796807006326 ↩
- 2.Rivas, E., & Jaskelioff, M. (2014). Notions of Computation as Monoids. CoRR, abs/1406.4823. https://arxiv.org/abs/1406.4823 ↩