Search code examples
haskellequational-reasoning

Haskell - How to transform map sum (map (x:) xss) to map (x+) (map sum xss)


Reading "Thinking Functionally with Haskell" I came across a part of a program calculation that required that map sum (map (x:) xss) be rewritten as map (x+) (map sum xss)

Intuitively I know that it makes sense ...

if you have some lists that you are going to sum but, before summing, to those same lists you are also going to add one element 'x', then that is the same as taking a list of sums of the origninal lists and adding x's value to each of them.

But I would like to know how to transform one into the other only using equational reasoning. I feel like I'm missing a law or rule that would help me understand.


Solution

  • Using the law

    map f (map g list) === map (f . g) list
    

    We can deduce

    map sum (map (x:) xss) =
    map (sum . (x:)) xss =
    

    eta-expand to give an argument to work with

    map (\xs -> sum . (x:) $ xs) xss =
    

    Substituting in for (f . g) x === f (g x)

    map (\xs -> sum (x:xs)) xs =
    

    Where

    sum (x:xs) = x + sum xs
    sum [] = 0
    

    so

    map (\xs -> sum (x:xs)) xss =
    map (\xs -> x + sum xs) xss =
    

    Substituting f (g x) === (f . g) x

    map (\xs -> (x +) . sum $ xs) xss =
    

    eta-reduce the lambda

    map ((x +) . sum) xss =
    

    The use the reverse of the first law from above

    map (x+) (map sum xss)