Why is this expression equal?

Question

I'm learning Haskell at the moment and I read a book called "Thinking Functionally With Haskell" and I can't really understand why this expression from the first chapter is true:

sum . map sum = sum . concat

Answer 1

Informally, this is just saying that because if addition is associative, it doesn't matter how you group the numbers you are adding. (a + b) + (c + d) is the same as (a + b + c + d).

---

Formally, we can use equational reasoning and structure induction to prove this for lists of any size. (See the end for quick definitions of these two processes.)

Assuming the following definitions of map, concat, sum, and (.):

1. map sum [] = []
2. map sum (a:as) = sum a : map sum as
3. concat [] = []
4. concat (a:as) = a ++ concat as
5. sum [] = 0
6. sum (a:as) = a + sum as
7. (f . g) x = f (g x)

To make the proof below a little simpler, we'll claim without an explicit proof (but see below) that

8. sum (a ++ b) == sum a + sum b

First we establish that the identity is true for empty lists.

(sum . map sum) [] == sum (map sum [])  -- (7)
                   == sum []            -- (1)
                   == sum (concat [])   -- (3)
                   == (sum . concat) [] -- (7)

(Note that we don't need definition 5, since an empty list is an empty list.)

Now, add a new definition, for any list as of size k.

9. (sum . map sum) as == (sum . concat) as

If (9) is true, we can prove the identity for list of size k+1:

(sum . map sum) (a:as) == sum (map sum (a:as))        -- (7)
                       == sum (sum a : map sum as)    -- (2)
                       == sum a + sum (map sum as)    -- (6)
                       == sum a + (sum . map sum) as  -- (7)
                       == sum a + (sum . concat) as   -- (9)
                       == sum a + sum (concat as)     -- (7)
                       == sum (a ++ concat as)        -- (8)
                       == sum (concat (a:as))         -- (4)
                       == (sum . concat) (a:as)       -- (7)

By induction, we have proved the sum . map sum == sum . concat for lists of any size.

---

• Equational reasoning means that we can use an equality like a = b to replace a with b or b with a at any step of our proofs.

• Structural induction on lists is a bootstrapping process. You assume some property is true for lists of size k, then use that to prove it is true for lists of size k+1. Then, if you can prove it is true for k=0, this implies it is true for all k. For example, if it is true for k=0, then it is true for k=1, which means it is true for k=2, etc.

---

Definition 4 assumes a definition of ++:

[] ++ bs = bs
(a:as) ++ bs = a : (as ++ bs)

With ++ defined, we can prove (8):

A base case: a is empty

sum ([] ++ b) == sum b               -- definition of ++
              == 0 + sum b           -- definition of +
              == sum [] + sum b      -- definition of sum

Assuming sum (a++b) is true for a of length k,

sum ((a:as) ++ bs) == sum (a : (as ++ bs))   -- definition of ++
                   == a + sum (as ++ bs)     -- definition of sum
                   == a + sum as + sum bs    -- induction
                   == sum (a:as) + sum bs    -- definition of sum

Answer 2

Imagine we have a list:

myList :: [[Int]]
myList = [[1,2],[3,4,5]]

Let's apply sum . map sum:

  (sum . map sum) [[1,2],[3,4,5]]
= sum [sum [1,2], sum [3,4,5]]
= sum [1+2,3+4+5]
= 1+2+3+4+5

Now let's apply sum . concat:

   (sum . concat) [[1,2],[3,4,5]]
 = sum [1,2,3,4,5]
 = 1+2+3+4+5

Hopefully you can see now that, because (a+b)+c = a+(b+c), the order in which we add things does not matter, thus summing the inner lists, then summing the entire list produces the same result as simply summing each value of the inner lists.