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 =&gt; M[B], g: B =&gt; M[C]): A =&gt; 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 =&gt; M[B]) = compose(_: Unit =&gt; x, f)(())


will satisfy

flatMap(flatMap(x)(f))(g) == flatMap(x)(a =&gt; 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 =&gt; unit(y), f)(())


If there was some rule like 

compose(_: Unit =&gt; 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 =&gt; 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)@&gt;h\odot -&gt;&gt;\mathcal{C}(A,MC) \\
@V-\circ gVV @VV-\circ gV \\
\mathcal{C}(X,MB) @&gt;&gt;h\odot -&gt; \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.