# Proving monad laws for flatMap and unit, given laws for compose and unit

I'll use scala notation but hopefully things will make sense in general (I'm trying to prove that you can define a monad using either [flatMap (aka bind) and unit] or [compose and unit])

The book Functional Programming in Scala (github at https://github.com/fpinscala/fpinscala) makes the claim that if we have a type constructor M and functions compose and unit

compose(f: A => M[B], g: B => M[C]): A => M[C]
unit(a: A): M[A]


satisfying

compose(compose(f, g), h) == compose(f, compose(g, h))
compose(f, unit) == f
compose(unit, f) == f


then defining a function flatMap

flatMap(x: M[A])(f: A => M[B]) = compose(_: Unit => x, f)(())


will satisfy

flatMap(flatMap(x)(f))(g) == flatMap(x)(a => flatMap(f(a))(g)
flatMap(x)(unit) == x
flatMap(unit(y))(f) == f(y)


I can't prove this. The easiest place to see my confusion is trying to show the last identity. We have

flatMap(unit(y))(f) = compose(_: Unit => unit(y), f)(())


If there was some rule like

compose(_: Unit => unit(y), f)(()) = compose(unit, f)(y)


or more generally

compose(f∘g, h)(a) = compose(f, h)(g(a))


then we could conclude that the identity is true, but as is, I don't see any move I'm allowed to make. Any ideas?

The solutions for this question https://github.com/fpinscala/fpinscala/blob/master/answerkey/monads/10.answer.scala only do the case where compose is defined in terms of flatMap but the questions asks "Prove that these two statements of the identity laws are equivalent" so I think the solutions should include both implications.

That rule you are asking for is (with slight tweaking) a naturality condition mathematically. It would be more naturally written as: $$\mathtt{compose}(f\circ g,h)=\mathtt{compose}(f,h)\circ g$$ If compose used the typical order for composition, you could write it more prettily as: $$(h\odot f)\circ g = h\odot(f\circ g)$$ where $h\odot f = \mathtt{compose}(f,h)$.

The type A => M[B] corresponds to the hom-functor for the Kleisli category of $M$, $\mathcal{C}_M(A,B)\equiv\mathcal{C}(A,MB)$. Given a Kleisli arrow $h : B \to MC$, we have the function $h\odot- : \mathcal{C}(A,MB)\to\mathcal{C}(A,MC)$, and this is natural in $A$. The naturality diagram is: $$\require{AMScd} \begin{CD} \mathcal{C}(A,MB)@>h\odot ->>\mathcal{C}(A,MC) \\ @V-\circ gVV @VV-\circ gV \\ \mathcal{C}(X,MB) @>>h\odot -> \mathcal{C}(X,MC) \end{CD}$$ where $g : X \to A$. (In fact, this can also be read as a naturality diagram for $-\circ g : \mathcal{C}_M(A,-)\to\mathcal{C}_M(X,-)$.) That $h\odot -$ is natural can be easily derived from its definition as $f\mapsto \mu\circ Mh \circ f$ where $\mu$ is the multiplication of the monad $M$, i.e. flatten, and $Mf$ is the functorial action of $M$, i.e. map.

At any rate, the equation you want would be a free theorem if Scala was a suitably nicely behaved language. Indeed, that Scala isn't "suitably nicely behaved" is an omnipresent problem and leads to many of these laws not actually holding. (This problem occurs with Haskell too, but not nearly so catastrophically.) I assume Paul and Runar discuss this and free theorems somewhere in the book. They're certainly aware of it.

Thank you Derek Elkins for your helpful answer. One thing I took away from your answer is that the equation I want might not be true in Scala, because it has "too many escape hatches for parametricity", as described in http://data.tmorris.net/talks/parametricity/b8e0cb9d7f5dcdf48ef18eb49fc84905ece6b8ec/parametricity.pdf

So I tried to find a counterexample, here is my (I hope successful) attempt. First we define Mon (short for Monad) as requiring compose and unit to be defined and then defining flatMap in terms of compose. The typeTags are needed for later (also I'd never really played with typeTags and implicits before so there are probably better ways to do it).

import scala.reflect.runtime.universe._
import language.higherKinds

trait Mon[M[_]] {
def compose[A, B, C](f: A => M[B], g: B => M[C])
(implicit tA: TypeTag[A], tB: TypeTag[B], tC: TypeTag[C]): A => M[C]

def unit[A](a: A): M[A]

def flatMap[A, B](ma: M[A])(f: A => M[B])
(implicit tA: TypeTag[A], tB: TypeTag[B]): M[B] =
compose((_: Unit) => ma, f)(typeTag[Unit], tA, tB)(())
}


Then we define Option to be a Mon as follows

val optMon: Mon[Option] = new Mon[Option] {
def unit[A](a: A): Option[A] = Some(a)

override def compose[A, B, C](f: A => Option[B], g: B => Option[C])
(implicit tA: TypeTag[A], tB: TypeTag[B], tC: TypeTag[C]): A => Option[C] =
(a: A) => if (tA.tpe == tB.tpe || tB.tpe == tC.tpe)
f(a).flatMap(g)
else
None
}


This defines unit in the normal way. The definition of compose in the 'natural' way would just be f(a).flatMap(g), but we use the ability of Scala to inspect the types, and define it to be the natural formula if A == B or B == C, otherwise just None.

We now show that optMon satisfies the three monad laws in terms of compose and unit:

compose(f: A => M[B], unit: B => M[B])
= (a: A) => f(a).flatMap(unit)
= (a: A) => f(a)
= f

compose(unit: A => M[A], f: A => M[B])
= (a: A) => Some(a).flatMap(f)
= (a: A) => f(a)
= f


For

compose(f: A => M[B], compose(g: B => M[C], h: C => M[D]))
= compose(compose(f, g), h)


note that the LHS is made to be None by our compose formula if (A != B and B != D) or (B != C and C != D). The RHS is made to be None if (A != B and B != C) or (A != C and C != D). One way the LHS can be forced to be None is if A != B and B != D. Then if B != C the RHS is forced to be None, otherwise B = C but then A != C and C != D so the RHS is forced to be None. Similar arguments show that if (A != C and C != D) is true then the RHS is forced to be None. Symmetrical arguments show that if the RHS is forced to be None then the LHS is forced to be None. When neither side is forced to be None then the equation is just the associativity law for a monad defined in terms of flatMap which is true.

Finally we show that flatMap (defined in terms of this compose) does not satisfy one of the identity laws.

flatMap(unit(""), (s: String) => Some(s.length))
= compose((_: Unit) => unit(""), (s: String) => Some(s.length))(())
= None // because A != B and B != C
!= ((s: String) => Some(s.length))("")
= Some(0)