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:

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

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

Just be methodical about it. You already have `1. Implementation. Applicative --> Monoidal`, `2. Implementation. Monoidal --> Applicative`. Now prove each Monoidal Law given the Applicative Laws and the `1.` implementation; then prove each Applicative Law given the Monoidal Laws and the `2.` implementation. At each proof, start with the premise, and arrive at the needed conclusion while carefully documenting at each step what known laws you've used to perform it. It's mechanical. If you want to get a feel about it, do it after you've written it all down. That's what I would do. — Will Ness, Jul 17 '20 at 13:25
so when we go about it slowly and carefully, we can be sure. vague reasoning gives no guarantees (unless you *really* know what you're saying). e.g. "`($ y) ≅ y`", I don't think this is right at all. — Will Ness, Jul 17 '20 at 14:08
@WillNess well, I did not try to do formal proofs (I will, as you suggested). Yet, I do not see why the isomorphism you mentioned does not hold. From left to right we have `\ t -> t id`; from right to left - `\ t -> ($ t)`. Where am I wrong? — Zhiltsoff Igor, Jul 17 '20 at 14:20
isomorphisms are between types but `y` and `($ y)` are values? perhaps I didn't quite get your meaning there. — Will Ness, Jul 17 '20 at 14:31
@WillNess yes, I was speaking of values. At least I have no knowledge of `$` type operator. I guess it was clumsy, but it seemed fitting for an intuition. Is this a bad way to put things? To be honest, all my experience of proofs of such sort are just, as you have said, mechanical work. If you could give me some example where such style is carried out right, I would appreciate it very much. — Zhiltsoff Igor, Jul 17 '20 at 14:47

score 8 · Answer 1 · answered Jul 17 '20 at 18:29

Just dumping this here for now... wanted to discuss this but I already spent way to long implementing it: it's a Coq proof script that shows the equivalence in an absolutely waterproof way.

Require Import Coq.Program.Basics.
Require Import Coq.Init.Datatypes.
Require Import Coq.Init.Notations.

Notation "f ∘ g" := (compose f g).

Class Functor (F: Type -> Type) : Type :=
  { fmap : forall {x} {y}, (x->y) -> (F x->F y)
  ; fmap_id : forall x, @fmap x x id = id
  ; fmap_compose : forall {x} {y} {z} (f: y->z) (g: x->y)
                     , fmap (f∘g) = fmap f ∘ fmap g
  }.

Lemma fmap_twice {F} `{Functor F} {x} {y} {z} (f: y->z) (g: x->y) (xs: F x)
                     : fmap (f∘g) xs = fmap f (fmap g xs).
Proof.
  rewrite fmap_compose. now compute.
Qed.

Definition parallel {a} {b} {c} {d} (f: a->c) (g: b->d)
  : (a*b) -> (c*d) := fun xy => match xy with
                                | (x,y) => (f x, g y)
                                end.

Notation "f *** g" := (parallel f g) (at level 40, left associativity).

Definition rassoc {a} {b} {c} : ((a*b)*c) -> (a*(b*c))
    := fun xyz => match xyz with | ((x,y),z) => (x,(y,z)) end.

Definition tt_ {a} (x:a) := (tt, x).
Definition _tt {a} (x:a) := (x, tt).

Class Monoidal F `{Functor F} : Type :=
  { funit : F unit
  ; fzip : forall {a} {b}, F a -> F b -> F (a*b)
  ; left_identity : forall {a} (v: F a)
           , fzip funit v = fmap tt_ v
  ; right_identity : forall {a} (v: F a)
           , fzip v funit = fmap _tt v
  ; associativity : forall {a} {b} {c} (u: F a) (v: F b) (w: F c)
           , fzip u (fzip v w) = fmap rassoc (fzip (fzip u v) w)
  ; naturality : forall {a} {b} {c} {d}
                        (g: a->c) (h: b->d) (u: F a) (v: F b)
           , fmap (g***h) (fzip u v) = fzip (fmap g u) (fmap h v)
  }.

Notation "u ** v" := (fzip u v) (at level 40, left associativity).

Lemma naturalityL {F} `{Monoidal F} {a} {b} {c}
                           (f: a->c) (u: F a) (v: F b)
           : fmap (f***id) (fzip u v) = fzip (fmap f u) v.
Proof.
  assert (v = fmap id v) as ->. { now rewrite fmap_id. }
  rewrite <- naturality.
  assert (v = fmap id v) as <-. { now rewrite fmap_id. }
  now trivial.
Qed.
Lemma naturalityR {F} `{Monoidal F} {a} {b} {c}
                           (f: b->c) (u: F a) (v: F b)
           : fmap (id***f) (fzip u v) = fzip u (fmap f v).
Proof.
  assert (u = fmap id u) as ->. { now rewrite fmap_id. }
  rewrite <- naturality.
  assert (u = fmap id u) as <-. { now rewrite fmap_id. }
  now trivial.
Qed.

Definition to {a} {b} (y: a) (f: a->b) := f y.

Class Applicative F `{Functor F} : Type :=
  { pure : forall {a}, a -> F a
  ; app : forall {a} {b}, F (a->b) -> F a -> F b
  ; identity : forall {a} (v: F a)
              , app (pure id) v = v
  ; homomorphism : forall {a} {b} (f: a->b) (x: a)
              , app (pure f) (pure x) = pure (f x)
  ; interchange : forall {a} {b} (u: F (a->b)) (y: a)
              , app u (pure y) = app (pure (to y)) u
  ; composition : forall {a} {b} {c}
                         (u: F (b->c)) (v: F (a->b)) (w: F a)
              , app u (app v w) = app (app (app (pure compose) u) v) w
  ; appFtor : forall {a} {b} (g: a->b) (x: F a)
              , fmap g x = app (pure g) x
  }.

Notation "fs <*> xs" := (app fs xs) (at level 40, left associativity).

Require Import Coq.Program.Tactics.
Require Import Coq.Logic.FunctionalExtensionality.

Definition apl {a} {b} (fx: (a->b)*a)
   := match fx with |(f,x) => f x end.

Program Instance MonoidalIsApplicative {F} `{Monoidal F}
    : Applicative F
  := { pure := fun {a} (x: a) => fmap (const x) funit
     ; app := fun {a} {b} (fs: F (a->b)) (xs: F a)
              => fmap apl (fzip fs xs) }.
Next Obligation. (* identity *)
  rewrite <- naturalityL.
  rewrite -> left_identity.
  repeat (rewrite <- fmap_twice).
  rewrite -> fmap_id.
  now compute.
Qed.
Next Obligation. (* homomorphism *)
  rewrite <- naturality.
  rewrite -> left_identity.
  repeat (rewrite <- fmap_twice).
  now compute.
Qed.
Next Obligation. (* interchange *)
  rewrite <- naturalityL.
  rewrite <- naturalityR.
  repeat (rewrite <- fmap_twice).
  rewrite -> right_identity.
  rewrite -> left_identity.
  repeat (rewrite <- fmap_twice).
  now compute.
Qed.
Next Obligation. (* composition *)
  rewrite <- naturalityR.
  rewrite -> associativity.
  repeat (rewrite <- naturalityL).
  rewrite -> left_identity.
  repeat (rewrite <- naturalityL).
  repeat (rewrite <- fmap_twice).

  f_equal.                      (*    This part is just about *)
  unfold compose.                 (*  convincing Coq that two  *)
  apply functional_extensionality. (* functions are equal, it  *)
  intro x.                         (* has nothing to do with   *)
  destruct x as ((btc, atb), a0). (*  applicative or monoidal  *)
  now compute.                  (*    functors, specifically. *)
Qed.
Next Obligation. (* appFtor *)
  rewrite <- naturalityL.
  rewrite -> left_identity.
  repeat (rewrite <- fmap_twice).
  now compute.
Qed.


Lemma fmapPure {F} `{Applicative F} {a} {b}
        (f: a->b) (x: a) : fmap f (pure x: F a) = pure (f x).
Proof.
  rewrite -> appFtor.
  now apply homomorphism.
Qed.

Lemma fmapBracket {F} `{Applicative F} {a} {b} {c} {d}
      (f: c->d) (g: a->b->c) (xs: F a) (ys: F b)
     : fmap f (fmap g xs<*>ys) = fmap (fun x y => f (g x y)) xs <*> ys.
Proof.
  repeat (rewrite -> appFtor).
  rewrite -> composition.
  rewrite -> homomorphism.
  rewrite -> composition.
  repeat (rewrite -> homomorphism).
  now compute.
Qed.

Lemma fmap_both {F} `{Applicative F} {a} {b} {c} {d}
      (f: a->c->d) (g: b->c) (xs: F a) (ys: F b)
     : fmap f xs <*> fmap g ys = fmap (fun x y => f x (g y)) xs <*> ys.
Proof.
  repeat (rewrite -> appFtor).
  rewrite -> composition.
  repeat (rewrite <- appFtor).
  rewrite <- fmap_twice.
  rewrite -> interchange.
  rewrite -> appFtor.
  rewrite -> composition.
  repeat (rewrite -> homomorphism).
  rewrite <- appFtor.
  now compute.
Qed.

Definition tup {a} {b} (x:a) (y:b) : (a*b) := (x,y).

Program Instance ApplicativeIsMonoidal {F} `{Applicative F}
    : Monoidal F
  := { funit := pure tt
     ; fzip := fun {a} {b} (u: F a) (v: F b)
                   => fmap tup u <*> v }.
Next Obligation. (* left_identity *)
  repeat (rewrite -> appFtor).
  rewrite -> homomorphism.
  now compute.
Qed.
Next Obligation. (* right_identity *)
  repeat (rewrite -> appFtor).
  rewrite -> interchange.
  rewrite -> composition.
  repeat (rewrite -> homomorphism).
  now compute.
Qed.
Next Obligation. (* associativity *)
  repeat (rewrite -> fmapBracket).
  rewrite -> composition.
  repeat (rewrite <- appFtor).
  rewrite <- fmap_twice.
  rewrite -> fmap_both.
  now compute.
Qed.
Next Obligation. (* naturality *)
  rewrite -> fmap_both.
  rewrite <- fmap_twice.
  rewrite -> fmapBracket.
  now compute.
Qed.

Compiled with Coq 8.9.1.

Will Ness · Accepted Answer · 2020-07-24T13:29:54.110

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.

score 1 · Answer 3 · answered Jul 19 '20 at 20:34

Following Will Ness's advice:

Here is what we get of Homomorphism (besides the laws spoken of about, I used the law specifying how Applicative should relate to Functor: fmap g x = pure g <*> x.)

pure f <*> pure x = 
= uncurry ($) <$> ((,) <$> (pure f) <*> (pure x)) = 
= (uncurry ($) .) <$> ((,) <$> (pure f)) <*> (pure x) =
= ((uncurry ($) .) . (,) <$> (pure f)) <*> (pure x) = 
= (uncurry ($) . (,) f) <$> (pure x) =
= pure $ (uncurry ($) . (,) f) x = 
= pure (f x)

So, I guess both Homorphism and fs <*> xs = uncurry ($) <$> (fs ** xs) enable us to perform application on the level of functors.

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

3 Answers3

Linked