Thank you <PERSON> 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). 945
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. 433