# Monoidal and Applicative Functors

In this posts we will explore the equivalence between applicative and monoidal functors (i.e. functors which preserve cartesian product).

`module Data.Functor.Monoidal where`

```
import Data.Functor (($>))
import Data.Functor.Identity (Identity (..))
```

## Monoidal categories

We will only focus on a basic example of a monoidal category. The prototypical example is category with products, e.g. the category `Hask`

together with `(,)`

type, and this is the category we will consider. A monoidal category also assumes a unit object and some laws for the monoidal product which look very familiar to those of a monoid, but slightly more general. A monoidal structure in a given category is a bit like a monoid, where you can combine any two objects of a category but the unitality and associativity laws have to be relaxed. They are satisfied up to an isomorphism. This is needed even in the simplest case as we have here where the monoidal product is simply given by the categorial product, i.e. the pair type `(a,b)`

.

*associativity*

```
assoc :: (a, (b, c)) -> ((a, b), c)
= ((a, b), c) assoc (a, (b, c))
```

*left unit*

```
leftUnit :: a -> ((), a)
= ((), a) leftUnit a
```

*right unit*

```
rightUnit :: a -> (a, ())
= (a, ()) rightUnit a
```

And these isomorphism have to satisfy additional, so called coherence conditions. This is all done for a greater generality, where one wants the monoidal product to keep reasonable simple. Since we’re not focused here on full introduction of monoidal categories, and we won’t need its coherence laws we will not dive into the details.

There are monoidal categories which monoidal product is different than the product, and this is probably more natural for many application in pure mathematics, especially in algebra (tensor product in linear algebra, smashed product in some topological context, or the category of endofunctors, …).

## Monoidal functors - definition

Since we now have a `Hask`

as an example of a monoidal category, we will be interested in functors that preserve this monoidal structure. They are called monoidal functors, and they are defined by the following type class.

```
class Functor f => Monoidal f where
unit :: f ()
(<|>) :: f a -> f b -> f (a, b)
infixl 4 <|>
```

Note that this definition expressese the notion of a monoidal endo-functors of the category `(->)`

in which the monoidal product is given by the tuple type `(a, b)`

.

## Monoidal functors - laws

Monoidal functors have to obey the following laws:

*left unit law*

`unit <|> fb = (unit,) <$> fb`

*right unit law*

`fa <|> unit = (,unit) <$> fa`

*naturality*

```
(f <$> fa) <|> fb = (\(a,b) -> (f a, b)) <$> (fa <|> fb)
fa <|> (f <$> fb) = (\(a,b) -> (a, f b)) <$> (fa <|> fb)
```

Thus

`unit <|> unit = (unit,) <$> unit = (,unit) <$> unit`

## Applicative functors

There’s no need to introduce applicative functors. Let me just cite the applicative functor laws, which we will use quite extensievly:

*identity law*

`pure id <*> v = v`

*composition law*

`pure (.) <*> u <*> v <*> w = u <*> (v <*> w)`

*homomorphism law*

`pure f <*> pure x = pure (f x)`

*interchange law*

`u <*> pure y = pure ($ y) <*> u`

We will now present an argument that *every applicative functor* is a functor for which the following *formula* holds:

`fmap f fa = pure f <*> fa`

**Lemma** If `f`

is an applicative functor then

```
liftA :: Applicative f => (a -> b) -> f a -> f b
= pure f <*> fa liftA f fa
```

satisfies functor laws.

**Proof**

```
liftA id fa
= pure id <*> fa
-- by identity law
= fa
```

```
liftA (f . g) fa
= pure (f . g) <*> fa
= pure ((.) f g) <*> fa
= pure (.) <*> pure f <*> pure g <*> fa
-- by composition law
= pure f <*> (pure g <*> fa)
= liftA f (liftA g fa)
```

QED

Any data structure has at most one functor instance, thus whenever one has a functor instance it must be the one. As a consequence for an applicative functor `fmap`

and `liftA`

are always equal. This allows us to use `liftA`

in exchange for `fmap`

in proofs. That’s very handy, since otherwise the applicative properties do not provide any compatiblity with `fmap`

.

It turns out that every applicative functor is a monoidal one. And this is thanks to the following standard definition of `monoidal`

and a bit further down `monoidalUnit`

:

```
-- | Every applicative functor is monoidal.
--
monoidal :: Applicative f
=> f a
-> f b
-> f (a, b)
= (,) <$> fa <*> fb monoidal fa fb
```

```
monoidalUnit :: Applicative f
=> f ()
= pure () monoidalUnit
```

```
instance Monoidal Identity where
= monoidalUnit
unit <|>) = monoidal
(
instance Monoidal IO where
= monoidalUnit
unit <|>) = monoidal (
```

But we still need to prove the monoidal laws.

**Monoidal laws of monoidal and monoidalUnit**

*left unit law*

```
monoidalUnit `monoidal` fb
= (,) <$> (pure ()) <*> fb
= pure (,) <*> pure () <*> fb
-- by homomorphism law
= pure ((),) <*> fb
= ((),) <$> fb
```

*right unit law*

```
fa `monoidal` monoidalUnit
= (,) <$> fa <*> pure ()
-- by interchange law
= pure ($ ()) <*> ((,) <$> fa)
= pure ($ ()) <*> (pure (,) <*> fa)
-- by composition law
= pure (.) <*> pure ($ ()) <*> pure (,) <*> pure fa
= pure ((.) ($ ()) (,)) <*> fa
= pure (\(a -> (a, ())) <*> fa
= pure (,()) <*> fa
= (,()) <$> fa
```

**Lemma**

`(\a b -> (f a, b)) <$> fa <*> fb = (\(a, b) -> (f a, b)) <$> ((,) <$> fa <$> fb)`

**Proof** It’s probably not a surprise that we will need to use applicative composition law. A first useful observation is that

```
(\a b -> (f a, b))
= (\g -> (\(a, b) -> (f a, b)) . g) . (\a b -> (a, b))
= ((.) (\(a, b) -> (f a, b))) . (\a b -> (a, b))
```

```
(\a b -> (f a, b)) <$> fa <*> fb
-- by the above observation
= (((.) (\(a, b) -> (f a, b))) . (\a b -> (a, b))) <$> fa <*> fb
-- by functor law
= ((.) (\(a, b) -> (f a, b))) <$> ((\a b -> (a, b)) <$> fa) <*> fb
= pure ((.) (\(a, b) -> (f a, b))) <*> ((\a b -> (a, b)) <$> fa) <*> fb
-- by applicative homomorphism law
= pure (.) <*> pure (\(a, b) -> (f a, b)) <*> ((\a b -> (a, b)) <$> fa) <*> fb
-- by applicative composition law
= pure (\(a, b) -> (f a, b)) <*> (((\a b -> (a, b)) <$> fa) <*> fb)
-- by applicative functor lemma
= (\(a, b) -> (f a, b)) <$> ((,) <$> fa <$> fb)
```

QED

*naturality laws*

```
(f <$> fa) `monoidal` fb
= (,) <$> (f <$> fa) <*> fb
= (,) <$> (pure f <*> fa) <*> fb
= pure (,) <*> (pure f <*> fa) <*> fb
-- by composition law
= pure (.) <*> pure (,) <*> pure f <*> fa <*> fb
-- by functor lemma
= pure ((.) (,) f) <*> fa <*> fb
= pure (\a b -> (f a, b)) <*> fa <*> fb
= (\a b -> (f a, b)) <$> fa <*> fb
= (\(a, b) -> (f a, b)) <$> ((\a b -> (a, b)) <$> fa <*> fb)
-- by previous lemma
= (\(a, b) -> (f a, b)) <$> ((,) <$> fa <*> fb)
= (\(a, b) -> (f a, b)) <$> (fa `monoidal` fb)
```

```
fa `monoidal` (f <$> fb)
= (,) <$> fa <*> (f <$> fb)
= ((,) <$> fa) <*> (pure f <*> fb)
-- by composition law
= pure (.) <*> ((,) <$> fa) <*> pure f <*> fb
= (.) <$> ((,) <$> fa)) <*> pure f <*> fb
-- by functor law
= (.) . (,) <$> fa <*> pure f <*> fb
-- by interchange law
= pure ($ f) <*> ((.) . (,) <$> fa) <*> fb
= pure ($ f) <*> (pure ((.) . (,)) <*> fa) <*> fb
-- by composition law
= pure (.) <*> pure ($ f) <*> pure ((.) . (,)) <*> fa <*> fb
= pure ((.) ($ f) ((.) . (,))) <*> fa <*> fb
= pure (\(a,b) -> (a, f b)) <*> fa <*> fb
= (\a b -> (a, f b)) <$> fa <*> fb
= (\(a, b) -> (a, f b)) . (,) <$> fa <*> fb)
-- by composition law
= (\(a, b) -> (a, f b)) <$> ((,) <$> fa <*> fb)
```

## From Monoidal to Applicative functors

```
-- | And conversely every monoidal functor is applicative.
--
monoidalAp :: Monoidal f
=> f (a -> b)
-> f a
-> f b
=
monoidalAp fab fa uncurry ($) <$> (fab <|> fa)
```

```
monoidalPure :: Monoidal f
=> a
-> f a
= unit $> a monoidalPure a
```

**Applicative laws of monoidalAp and monoidalPure**

*homomorphism law*

```
monoidalPure ab `monoidalAp` monoidalPure a
= uncurry ($) <$> ((unit $> ab) <|> (unit $> a))
= uncurry ($) <$> ((const ab <$> unit) <|> ((const a <$> unit)))
= uncurry ($) <$> (\_ -> (ab, a)) <$> (unit <|> unit)
= uncurry ($) . (\_ -> (ab, a)) <$> (unit <|> unit)
= const (ab a) <$> (unit <|> unit)
by the fact that that (const a) <$> f == (const b) <$> g for any
`f, g :: f a`
= const (ab a) <$> unit
by definition of ($>)
= unit $> (ab a)
= monoidalPure (ab a)
```

QED

*identity law*

```
monoidalPure id `monoidalAp` f
= uncurry ($) <$> ((unit $> id) <|> f)
by /naturality/ (and the definition of @'$>'@
= uncurry ($) <$> (\(_, b) -> (id, b)) <$> (unit <|> f)
= uncurry ($) . (\(_, b) -> (id, b)) <$> (unit <|> f)
= (\(_, b) -> b) <$> (unit <|> f)
by /right unit/ law
= (\(_, b) -> b) <$> ((),) <$> f
= (\(_, b) -> b) . ((),) <$> f
= id <$> f
= f
```

QED

*interchange law*, i.e. `u <*> pure y = pure ($ y) <*> u`

```
u `monoidalAp` (monoidalPure y)
= uncurry ($) <$> (u <|> (unit $> y))
= uncurry ($) <$> (\(x, ) -> (x, y)) <$> (u <|> unit)
= uncurry ($) . (\(x, _) -> (x, y)) <$> (u <|> unit)
= (\(x, _) -> x y) <$> (u <|> unit)
= (\(x, _) -> x y) <$> (,()) <$> u
= (\(x, _) -> x y) . (,()) <$> u
= (\(x, _) -> x y) . (,()) <$> (\(_, x) -> x) <$> (unit <|> u)
= (\(x, _) -> x y) . (,()) . (\(_, x) -> x) <$> (unit <|> u)
= (\(_, x) -> x y) <$> (unit <|> u)
= uncurry ($) . (\(_, x) -> ($ y, x)) <$> (unit <|> u)
= uncurry ($) <$> (\(_, x) -> ($ y, x)) <$> (unit <|> u)
= uncurry ($) <$> ((unit $> ($ y)) <|> u)
= uncurry ($) <$> ((monoidalPure ($ y)) <|> u))
= (monoidalPure ($ y)) `monoidalAp` u
```

QED

*composition law* i.e. `pure (.) <*> u <*> v <*> w = u <*> (v <*> w)`

```
monoidalPure (.) `monoidalAp` u `monoidalAp` v `monoidalAp` w
= (uncurry ($) <$> ((unit $> (.)) <|> u)) `monoidalAp` v `monoidalAp` w
= uncurry ($)
<$> ((uncurry ($)
<$> ((unit $> (.)) <|> u)) <|> v)
`monoidalAp` w
= uncurry ($)
<$> (\((x,y),z) -> (x y, z))
<$> ((unit $> (.)) <|> u <|> v)
`monoidalAp` w
= uncurry ($) . (\((x,y),z) -> (x y, z))
<$> ((unit $> (.)) <|> u <|> v)
`monoidalAp` w
= (\((x,y),z) -> x y z)
<$> ((unit $> (.)) <|> u <|> v)
`monoidalAp` w
= (\(x,y) -> x . y)
<$> (u <|> v)
`monoidalAp` w
= uncurry (.) <$> (u <|> v) `monoidalAp w
= uncurry ($)
<$> (uncurry (.) <$> (u <|> v)) <|> w
= uncurry ($) . (\((x,y),z) -> (x . y, z))
<$> (u <|> v <|> w)
= (\((x,y),z) -> x . y $ z)
<$> (u <|> v <|> w)
= (\((x,y),z) -> x (y z))
<$> (u <|> v <|> w)
= uncurry (.)
<$> (u <|> v <|> w)
```

And from the other side:

```
u `monoidalAp` (v `monoidalAp` w)
= uncurry ($) <$> (u <|> (v `monoidalAp` w))
= uncurry ($) <$> (u <|> (uncurry ($) <$> (u <|> w)))
= uncurry ($) <$> (\((x,y) -> (x, uncurry ($) y)))
<$> (u <|> (u <|> w))
= uncurry ($) . (\((x,y) -> (x, uncurry ($) y))
<$> (u <|> (v <|> w))
= (\((x, y) -> x (uncurry ($) y)))
<$> (u <|> (v <|> w))
= (\(x, (y, z) -> x (y z))
<$> (u <|> (v <|> w))
= (\(x, (y, z) -> x (y z)) . (\((x,y),z) -> (x,(y,z)))
<$> (u <|> v <|> w)
= (\((x,y),z) -> x (y z))
<$> (u <|> v <|> w)
= uncurry (.)
<$> (u <|> v <|> w)
```

QED

# Equivalence between Applicative and Monoidal functors

## From applicative functor to monoidal and back

In this section we consider an applicative functor `f`

and we consider tha applicative `monoidalAp`

and `monoidalUnit`

obtained from the associated monoidal functor. We show that these are equal to what we start with `<*>`

and `pure`

of `f`

.

The strategy of the proof transform all `<$>`

into `<*>`

using `f <$> x = pure f <*> x`

and mobe all brackets to the left using the composition law of applicative functors.

When we’ll get to the above canonical form (brackets grouped to the left) this will be all based on:

**Lemma 1**

` (.) (uncurry ($)) . (,) = ($)`

**Proof**

```
((.) (uncurry ($)) . (,)) f a =
by definition of (.)
= (\x -> (.) (uncurry ($)) (x,)) f a
= (\x -> (uncurry ($)) . (x,)) f a
by definiiton of (.)
= (\x y -> (uncurry ($)) (x, y)) f a
by eta reduction
= uncurry ($) (f, a)
= ($) f a
= f a
```

QED

Below we show that if we take `monoidalAp`

defined via `<|>`

which is defined by `monoidalAp`

(which we denote by `<*>`

to make all the expressions shorter), then we will recover our original applicative `<*>`

(e.g. `monoidalAp`

):

```
monoidalAp fab fa
-- by definition of `monoidalAp`
= uncurry ($) <$> (fab <|> fa)
-- by defintion of `<|>`
= uncurry ($) <$> ((,) <$> fab <*> fa)
= uncurry ($) <$> (pure (,) <*> fab <*> fa)
= pure (uncurry ($)) <*> ((pure (,) <*> fab) <*> fa)
by composition
= pure (.) <*> pure (uncurry ($)) <*> (pure (,) <*> fab) <*> fa
= pure ((.) (uncurry ($))) <*> (pure (,) <*> fab) <*> fa
by lemma 2
= fab <*> fb
```

**Lemma 2**

`pure ((.) (uncurry ($))) <*> (pure (,) <*> fab) = fab`

**Proof**

```
pure ((.) (uncurry ($))) <*> (pure (,) <*> fab)
by /composition law/ of applicative functors
= pure (.) <*> pure ((.) (uncurry ($))) <*> pure (,) <*> fab
= pure ((.) ((.) (uncurry ($)))) <*> pure (,) <*> fab
= pure ((.) ((.) (uncurry ($))) (,)) <*> fab
= pure (((.) (uncurry ($))) . (,)) <*> ab
by lemma 1
= pure ($) <*> fab
since ($) = (id :: (a -> b) -> (a -> b)
and (pure id) <*> x = x
= fab
```

QED

## From monoidal to applicative and back

In this section we consider a monoidal functor `f`

, and then we consisder tha monoidal functor obtained from the associated applicative functor by means of `monoidalAp`

and `monoidalUnit`

. We prove that what we end with is the initial monoidal functor `f`

. We use `<|>`

and `unit`

to denote the initial monoidal structer of `f`

, `<*>`

and `pure`

is the associated applicative instance, and we will show that `monoidal`

is equal to `<|>`

```
monoidal fa fb
= (,) <$> fa <*> fb
= ((,) <$> fa) <|> fb)
= uncurry ($) <$> ((,) <$> fa) <|> fb
= uncurry ($) <$> (fmap (\(a, b) -> ((a,),b)) <$> (fa <|> fb))
= uncurry ($) . (\(a, b) -> ((a,),b) <$> (fa <|> fb)
= id <$> (fa <|> fb)
= fa <|> fb
```

```
monoidalUnit
= pure ()
-- by definition of pure for the associated applicative functor
= monoidalPure ()
= unit $> ()
= unit
```

# References

Applicative Programming with Effects, Conor McBride and Ross Peterson, Journal of Functional Programming, 2008.

There is a final section which briefly mentions equivalnce between strict lax monoidal functors and applicative ones (without all the details we went through here). It touches some subtle difference between categorical formulation and a higher order functional perspective (also used here), which are byond this blog post.