I am reading Functional Programming in Scala, where I have been asked to prove the map fusion law. Since Scala is what I am familiar with, I am using as my notation a kind of pseudo-Scala.
Here is the text of the question, from the book:
Given map(y)(id) == y, it's a free theorem that map(map(y)(g))(f) == map(y)(f compose g). (This is sometimes called map fusion, and it can be used as an optimization - rather than spawning a separate parallel computation to compute the second mapping, we can fold it into the first mapping.) Can you prove it? You may want to read the paper "Theorems for Free!" (http://mng.bz/Z9f1) to better understand the "trick" of free theorems.
I was unable to make much headway without assistance, so I tried searching online. I haven't been able to find anyone who has the text of the proof outlined in full, but there are several places where the proof is left as an exercise to the reader, with the useful hint to assume that y == x::xs (some List).
Here is my proof based on the assumption that y is some List:
We have to prove that map(map(y)(g))(f) == map(y)(f compose g) searching online, it appears that an important assumption is to assume y is of the form x0::xs0 so y is of the form x0::xs0 x0::x1::xs1 x0::x1::x2::xs2 ... x0::x2::xs2 ... ::xsn::Nil Proof: First we show map(y)(g) == g(x0)::g(x1)::g(x2) ... ::g(xn)::Nil map(y)(g) map(x0::xs)(g) g(x0)::map(xs0)(g) g(x0)::g(x1)::g(x2) ... ::g(xn)::Nil Now we prove map(map(y)(g))(f) == map(y)(f compose g) Starting from LHS, we manipulate until we have RHS map(map(y)(g))(f) map(g(x0)::g(x1)::g(x2) ... ::g(xn)::Nil)(f) f(g(x0))::map(g(x1)::g(x2)::g(x3):: ... ::g(xn)::Nil)(f) f(g(x0))::f(g(x1))::f(g(x2)):: ... ::f(g(xn))::Nil (f compose g)(x0)::(f compose g)(x1)::(f compose g)(x2):: ... ::(f compose g)(xn)::Nil map(x0::x1::x2 ... ::xn::Nil)(f compose g) map(y)(f compose g)
It occurs to me that the proof can be written in a way that uses structural induction, but I am not familiar enough with the technique to use it. Can anyone help with this? Also, can anyone recover the form of the solution that makes use of the identity law map(y)(id) == y as it is asked in the text of the problem? My answer is probably not what the authors had in mind when they posed the question.