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]
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)(())
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.