# Monoidal and Applicative Functors

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

IDEA: make a framework, which type checks all the proofs; maybe use liquid haskell for that.

module Data.Functor.Monoidal where

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 extensively: 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
liftA f fa = pure 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 compatibility 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)
monoidal fa fb = (,) <$> fa <*> fb monoidalUnit :: Applicative f => f () monoidalUnit = pure () instance Monoidal Identity where unit = monoidalUnit (<|>) = monoidal instance Monoidal IO where unit = monoidalUnit (<|>) = 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 monoidalPure a = unit$> 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 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 move 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 definition 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 definition 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 consider the 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 structure 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`
• Monoidal Categories in ncatlab.org

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

There is a final section which briefly mentions equivalence 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 beyond this blog post.