# 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.

The interesting question is how to prove the equivalence (and what that equivalence actually means) under some required restrictions.

The required restrictions are that your function's code must be "fully parametric": use only type parameters and never any specific types; no run-time identification of type parameters; no reflection; and of course no side effects. Of course you can make an example in Scala (and in Haskell, etc.) where the functions do not satisfy the law because they identify types at run time. But it's a case that almost never comes up in practice.

What you are missing for your proof is a naturality law of compose. Without assuming that law, it is not true that flatMap(unit(y))(f) == f(y).

Naturality laws will hold automatically whenever the code is "fully parametric", i.e., restricted in the way I just described. But this is a complicated subject that currently has no good tutorials available. For instance, the "Theorems for free" paper is certainly not suitable as a tutorial for a practicing Scala or Haskell programmer trying to understand how to prove - or even how to write - a naturality law for compose.

So, let us just assume that the following additional "left naturality" law holds for compose:

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


Now we have:

 flatMap(unit(y))(f)
==  compose(_: Unit => unit(y), f)(())
== compose( (_ => y) andThen unit, f)(())  // Now use the left naturality law of compose.
== ((_ => y) andThen compose(unit, f))(())
== ((_ => y) andThen f)(())
== ((_ => f(y))(())
== f(y)


The other laws of flatMap can be also derived from the laws of compose only by assuming a naturality law of compose.

The book "Functional programming in Scala" never mentions this additional assumption - neither in the chapter on monads nor in the chapter on applicatives, where a similar equivalence holds between "ap" and "zip" but only when certain naturality laws are assumed.

For the flatMap and compose, the authors of "FPiS" show you the proof of laws only in the direction where no additional assumptions are needed: namely, when compose is defined via flatMap. So, I guess, the authors never tried themselves proving those laws in the other direction.

The equivalence between compose and flatMap is explained in detail (but using a special, better adapted notation) in Section 10.2.6 of my book "The Science of Functional Programming". LyX/LaTeX source: https://github.com/winitzki/sofp pdf: https://leanpub.com/sofp

In my book, I go through a large number of derivations where one function type is equivalent to another. In each case, I find that there are extra naturality laws that one has to assume. Intuitively, this makes sense, because how else can a function flatMap with two type parameters be equivalent to a function compose with three type parameters? Only when compose is additionally constrained by a law that can arbitrarily modify one of its type parameters and so cancels the additional freedom of having one more type parameter.

The easiest example of "equivalence under naturality" is the equivalence of pure[A]: A => M[A] and u: M[Unit]. You can define pure(x) = u.map(_: Unit => x) and u = pure(()) but this does not already prove an equivalence between the types of these functions.

Indeed, they cannot be simply equivalent: pure[A] has a type parameter A but u has no type parameters.

So, in fact, they are equivalent only we assume a naturality law for pure:

  for all x: A, f: A => B:
pure(x).map(f) = pure(f(x))


Only with this additional law, one can prove that defining pure via u and back gives indeed an isomorphism in both directions.

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)