If M is a Monad then for any A, the set of `A => M[A]` forms a monoid

MonoidFromMonad.md

Claim: If M is a Monad, then for any type A, the set of A => M[A] forms a monoid

Reminder

• A monad can defined:

trait Monad[M[_]] {
  def pure[A](a: A): M[A]
  def flatMap[A](m: M[A])(f: A => M[B]): M[B]
}

• A monad respects the left-unit, right-unit & associative monad laws which are:
  • Left unit: for any (a: A) & for any (f: A => M[B]), Monad.flatMap(Monad.pure(a))(f) = f(a)
  • Right unit: for any (m: M[A]) & for any (f: A => M[B]), Monad.flatMap(m)(Monad.pure)(f) = m
  • Associative: for any (m: M[A]), (f: A => M[B]) & (g: B => M[C]), Monad.flatMap(Monad.flatMap(m)(f))(g) = Monad.flatMap(m)((a: A) => Monad.flatMap(f(a))(g))

Notation

• Let's call M_A = {f | f: A => M[A]}

What we want to prove

• There exists an operation + and an element 0 ∈ M_A such that (M_A, +, 0) forms a monoid, i.e it respects the laws:
  • + is a function (A => M[A], A => M[A]) => A => M[A]
  • associativity: ∀(a, b, c) ∈ M_A^3, a + (b + c) = (a + b) + c
  • identity element: ∀a ∈ M_A, 0 + a = a + 0 = a

Proof

• Because M is a monad, there exists one object that satisfies the Monad[M] trait - for simplicity, we'll just call that object M.

• Let's define 0 = M.pure

• Let's define + such that:

def +[A, M[_]](f: A => M[A], g: A => M[A])(implicit ev: Monad[M]): A => M[A] = 
  (a: A) => ev.flatMap(f(a))(g)

• + is clearly a (A => M[A], A => M[A]) => A => M[A] function

• The monoid identity property come directly from the left-unit + right-unit monad properties.

• The monoid associative property come directly from the monad associative property.