0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.