Why are Monoidal and Applicative laws telling us the same thing?

Question

I have learnt about Monoidal being an alternative way to represent Applicative not so long ago. There is an interesting question on Typeclassopedia:

3. (Tricky) Prove that given your implementations from the first exercise [pure and (<*>) written down using unit and (**) and the other way around], the usual Applicative laws and the Monoidal laws stated above are equivalent.

Here are these classes and laws:

-- A note from https://wiki.haskell.org/Typeclassopedia#Alternative_formulation:
-- In this and the following laws, ≅ refers to isomorphism rather than equality. 
-- In particular we consider (x,()) ≅ x ≅ ((),x) and ((x,y),z) ≅ (x,(y,z)).

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

-- unit ** v ≅ v - Left Identity.
-- u ** unit ≅ u - Right Identity.
-- u ** (v ** w) ≅ (u ** v) ** w - Associativity.

-- Applicative. 
class Functor f => Applicative f where
  pure  :: a -> f a
  infixl 4 <*>, ...
  (<*>) :: f (a -> b) -> f a -> f b
  ...

-- pure id <*> v = v - Identity.
-- pure f <*> pure x = pure (f x) - Homomorphism.
-- u <*> pure y = pure ($ y) <*> u - Interchange.
-- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w - Composition.

Writing down combinators using others is no big deal:

unit   = pure ()
f ** g = (,) <$> f <*> g = liftA2 (,) f g

pure x  = const x <$> unit
f <*> g = uncurry ($) <$> (f ** g)

Here is my understanding of why the laws are telling us the same thing:

u <*> pure y = pure ($ y) <*> u -- Interchange: Applicative law.

The first thing we shall notice is that ($ y) ≅ y (more formally: (y -> a) -> a ≅ y). Having that in mind, Interchange law simply tells us that (a, b) ≅ (b, a).

pure id <*> v = v -- Identity: Applicative law.

I reckon id to be something of a unit itself as it is the only inhabitant of type forall a. a -> a. Therefore, this law gives us the Left Identity:

unit ** v = v -- Left Identity: Monoidal law.

Now we can use that (a, b) ≅ (b, a) to write the Right Identity down:

u ** unit = u -- Right Identity: Monoidal law.

The Composition law:

u <*> (v <*> w) = pure (.) <*> u <*> v <*> w -- Composition: Applicative law.

I reckon this law to tell the same thing as Associativity for Monoidal:

u ** (v ** w) ≅ (u ** v) ** w

That is, (a, (b, c)) ≅ ((a, b), c). Applicative just adds a layer of application.

So, we have covered all of the Monoidal laws. I believe there is no need to do it the other way around as we are going to use the same isomorphisms. But one could have noticed something odd - we did not use the Homomorphism Applicative law:

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

I tried understanding Homomorphism in terms of the Naturality free theorem for Monoidal:

fmap (g *** h) (u ** v) = fmap g u ** fmap h v

But it seems odd as Homomorphism does not deal with side-effects, yet Naturality works with them just fine.

So, I have 3 questions:

1. Is my reasoning right?
2. Where does Homomorphism stand in this picture?
3. How can we understand the Naturality free theorem in terms of Applicative?

Answer 1

We have

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

-- unit ** v ≅ v - Left Identity.
-- u ** unit ≅ u - Right Identity.
-- u ** (v ** w) ≅ (u ** v) ** w - Associativity.

-- Applicative,
class Functor f => Applicative f where
  pure  :: a -> f a
  infixl 4 <*>
  (<*>) :: f (a -> b) -> f a -> f b

-- pure id <*> v = v - Identity.
-- pure f <*> pure x = pure (f x) - Homomorphism.
-- u <*> pure y = pure ($ y) <*> u - Interchange.
-- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w - Composition.

Implementation 1. Applicative --> Monoidal

unit     = pure ()
xs ** ys = pure (,) <*> xs <*> ys

Implementation 2. Monoidal --> Applicative

pure x  = const x <$> unit
fs <*> xs = uncurry ($) <$> (fs ** xs)

Now prove Monoidal Laws given Applicative Laws and Implementation 1:

Left Identity. unit ** v ≅ v

unit ** v = pure () ** v
          = pure (,) <*> pure () <*> v
          = pure (\x -> (,) () x) <*> v
          = pure (\x -> (() , x)) <*> v
          = pure (() ,) <*> v
          ≅ pure id <*> v
          = v

Right Identity. u ** unit ≅ u

u ** unit = u ** pure ()
          = pure (,) <*> u <*> pure ()
          = pure ($ ()) <*> (pure (,) <*> u)  -- u <*> pure y = pure ($ y) <*> u 
          -- u <*> (v <*> w) = pure (.) <*> u <*> v <*> w
          = pure (.) <*> pure ($ ()) <*> pure (,) <*> u
          = pure ((.) ($ ())) <*> pure (,) <*> u
          = pure ((.) ($ ()) (,)) <*> u
          = pure (\x -> (.) ($ ()) (,) x) <*> u
          = pure (\x -> ($ ()) ((,) x)) <*> u
          = pure (\x -> (,) x ()) <*> u
          = pure (\x -> (x , ())) <*> u
          = pure (, ()) <*> u
          ≅ pure id <*> u
          = u

Associativity. u ** (v ** w) ≅ (u ** v) ** w

u ** (v ** w) = ......

You should be able to continue this. I hope I didn't make any mistakes here, but if I did, correct them.