A personal blog about computer science topics.

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

Functor Functor Applicative Applicative Functor->Applicative Traversable Traversable Functor->Traversable Applicative->Traversable Alternative Alternative Applicative->Alternative Monad Monad Applicative->Monad Apply Apply Apply->Applicative Semigroup Semigroup Semigroup->Apply Monoid Monoid Semigroup->Monoid MonadPlus MonadPlus Monad->MonadPlus MonadFix MonadFix Monad->MonadFix ArrowApply ArrowApply Monad->ArrowApply Monoid->Applicative Monoid->Alternative Monoid->Monad Monoid->MonadPlus Category Category Monoid->Category ArrowPlus ArrowPlus Monoid->ArrowPlus Foldable Foldable Monoid->Foldable Arrow Arrow Category->Arrow Foldable->Traversable Arrow->ArrowApply ArrowChoice ArrowChoice Arrow->ArrowChoice ArrowZero ArrowZero Arrow->ArrowZero ArrowZero->ArrowPlus

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

  • ϕ A , B : F A F B F ( A B ) \phi_{A,B} : FA \otimes FB \rightarrow F(A \otimes B) (a natural transformation)

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}
\begin{xy} \xymatrix{ FA\ \otimes\ 1_{\mathcal{C}}\ar[d]_{\rho} \ar[r]^{FA\ \otimes\ \eta\ \ \ \ \ } & FA\ \otimes\ F(1_{\mathcal{C}}) \ar[d]^{\phi_{A,1_{\mathcal{C}}}} \\ FA & F(A\ \otimes\ 1_{\mathcal{C}}) \ar[l]_{F_{\rho}} } \end{xy}
\begin{xy} \xymatrix{ 1_{\mathcal{C}}\ \otimes\ FB\ar[d]_{\lambda} \ar[r]^{\eta\ \otimes\ FB\ \ \ \ } & F(1_{\mathcal{C}})\ \otimes\ F\ B \ar[d]^{\phi_{1_{\mathcal{C},B}}} \\ FB & F(1_{\mathcal{C}}\ \otimes\ B) \ar[l]_{{F_{\lambda}}} } \end{xy}

The 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 where 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]


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@C-=1cm{ \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(A) ⊗ F(B) -> F(A ⊗ B)
  (**) :: (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.

Though the compiler does not enforce it, a proper instance of Applicative should comply with the applicative laws:

pure id <*> a = a                              -- identity
pure (.) <*> a <*> b <*> c = a <*> (<*> c)   -- composition
pure f <*> pure a = pure (f a)                 -- homomorphism<*> pure b = pure ($ b) <*> a                -- interchange

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]

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

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

ghci> Just (*2) <*> Nothing


  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.