beuke.org

A personal blog about computer science topics.

Applicative
A Strong Lax Monoidal Endofunctor
Posted on Sep 8 2023 ~ 7 min read
#category theory  #haskell 



An applicative, in category theory, is a lax monoidal endofunctor with tensorial strength. Let ( C , , 1 C ) (\mathcal{C}, \otimes, 1_{\mathcal{C}}) be a monoidal category. A lax monoidal endofunctor is a functor F : C C F : \mathcal{C} \rightarrow \mathcal{C} together with two coherence maps:

  • η : 1 C F ( 1 C ) \eta : 1_{\mathcal{C}} \rightarrow F(1_{\mathcal{C}}) (the unit morphism)

  • ϕ X , Y : F X F Y F ( X Y ) \phi_{X,Y} : FX \otimes FY \rightarrow F(X \otimes Y) (a natural transformation)

such that the following diagrams commute:

\begin{xy} \xymatrix{ (FX\ \otimes\ FY)\ \otimes\ FZ \ar[r]^{\alpha} \ar[d]_{\phi_{X,Y}\ \otimes\ FZ} & FX\ \otimes\ (FY\ \otimes\ FZ) \ar[d]^{FX\ \otimes\ \phi_{Y,Z}} \\ F(X\ \otimes\ Y)\ \otimes\ FZ \ar[d]_{\phi_{X\ \otimes\ Y,Z}} & FX\ \otimes\ F(Y\ \otimes\ Z) \ar[d]^{\phi_{X,Y\ \otimes\ Z}} \\ F((X\ \otimes\ Y)\ \otimes\ Z) \ar[r]_{F_{\alpha}} & F(X\ \otimes\ (Y\ \otimes\ Z)) \\ } \end{xy}
\begin{xy} \xymatrix{ FX\ \otimes\ 1_{\mathcal{C}}\ar[d]_{\rho} \ar[r]^{FX\ \otimes\ \eta\ \ \ \ \ } & FX\ \otimes\ F(1_{\mathcal{C}}) \ar[d]^{\phi_{X,1_{\mathcal{C}}}} \\ FX & F(X\ \otimes\ 1_{\mathcal{C}}) \ar[l]_{F_{\rho}} } \end{xy}
\begin{xy} \xymatrix{ 1_{\mathcal{C}}\ \otimes\ FY\ar[d]_{\lambda} \ar[r]^{\eta\ \otimes\ FY\ \ \ \ } & F(1_{\mathcal{C}})\ \otimes\ F\ Y \ar[d]^{\phi_{1_{\mathcal{C},Y}}} \\ FY & F(1_{\mathcal{C}}\ \otimes\ Y) \ar[l]_{{F_{\lambda}}} } \end{xy}

The different natural transformations, α : ( a b ) c   a ( b c ) \alpha : (a \otimes b) \otimes c\ \rightarrow a \otimes (b \otimes c) (associativity), ρ : a 1 C a \rho : a \otimes 1_{\mathcal{C}} \rightarrow a (right identity), λ : 1 C a a \lambda : 1_{\mathcal{C}} \otimes a \rightarrow a (left identity) are part of the monoidal structure on C {\mathcal {C}} .

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 every functor is an endofunctor and every functor applied to the monoidal category S e t \mathbf{Set} , with the tensor product replaced by cartesian product, inherently possesses a unique strength, resulting in every functor within S e t \mathbf{Set} 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 S e t \mathbf{Set} 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)

class Functor f => Monoidal f where
  unit :: f ()
  (**) :: f a  -> f b  -> f (a, b)

Please note that fa -> fb -> f(a, b) is actually the curried version of
(f a, f b) -> f (a, b)

curry :: ((a, b) -> c) -> a -> b -> c
curry f x y = f (x, y)

uncurry :: (-> b -> c) -> (a, b) -> c
uncurry f p =  f (fst p) (snd p)

Haskell comes with curry and uncurry as part of its standard library, which together form an isomorphism.

\begin{xy} \xymatrix { \texttt{(a, b) -> c} \ar@/^1.5pc/[rr]^{\texttt{curry}} && \texttt{a -> b -> c} \ar@/^1.5pc/[ll]^{\texttt{uncurry}}} \end{xy}

Hence we can also phrase Monoidal this way, and it aligns seamlessly with our categorical definition of a strong lax monoidal functor:

class Functor f => Monoidal f where
-- η     : 1  -> F(1) (unit)
  unit :: () -> f ()
-- ϕx,y  : F(X) ⊗ F(Y) -> F(X ⊗ Y)
  (**) :: (f a, f b)   -> f (a, b)

We have the usual monoidal laws (pseudocode):

unit ** v == v == v ** unit    -- Left and Right Identity** (** w) == (** v) ** w -- Associativity

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)

class Applicative f where
  pure :: a -> f a
  (<*>) :: f (-> b) -> f a -> f b

This is how to recover Applicative in terms of Monoidal:

pure :: Monoidal f => a -> f a
pure x  = fmap (const x) unit

(<*>) :: Monoidal f => f (-> b) -> f a -> f b
f <*> g = fmap uncurry ($) (** g)

And this is the reverse direction, Monoidal in terms of Applicative:

unit :: Applicative f => f ()
unit   = pure ()

(**) :: Applicative f => f a -> f b  -> f (a, b)** g = fmap (,) f <*> g

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. Now, lets have a look at some instances of Applicative.

An Instance of Applicative, the List Applicative

instance Functor [] where
 -- pure :: a -> [a]
    pure x    = [x]

 --   (<*>) :: [(a -> b)] -> [a] -> [b]
    fs <*> xs = [f x | f <- fs, x <- xs]
 -- Thats a list comprehension that generates a new list
 -- by applying the function f to each element in the list
 -- xs for every function f in the list fs.

Another Instance, the Maybe Functor

instance Applicative Maybe where
 -- pure :: a -> Maybe a
    pure x                = Just (x)

 -- (<*>) :: Maybe (a -> b) -> Maybe a -> Maybe b
    (Just f) <*> (Just x) = Just (f x)
    _        <*> _        = Nothing

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.

ghci> [(*2)] <*> [1,2,3]
[2,4,6]

ghci> [(+1),(*2)] <*> [1,2,3]
[2,3,4,2,4,6]

ghci> Just (*2) <*> Just (3)
6

ghci> Just (*2) <*> Nothing
Nothing

References


  1. 0.The diagram displayed at the top of this post is a modified version of Brent Yorgey's Typeclassopedia diagram
  2. 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
  3. 2.Rivas, E., & Jaskelioff, M. (2014). Notions of Computation as Monoids. CoRR, abs/1406.4823. https://arxiv.org/abs/1406.4823