Two Different Ways of Thinking

Look again at our list appending function:

There are two ways to think about this computation. One way is to imagine the actions the computer might take to calculate the result:

Look at the first list. If it is empty, return the second list. Otherwise, pull apart the first list, looking at its head and tail. Make a recursive call to append the tail to the second list, and then cons the head onto the result. Return this.

Alternatively, we can consider each match case to be an independent statement of truth, thinking the same way about the whole function:

The empty list appended to another list is that list. Otherwise, the first list is non-empty, so it has a head and a tail. Call them h and t. Clearly append (h :: t) b is equal to h :: append t b. Since this reduces the problem size, progress is made.

It is very useful to be able to think in these two ways about functions you write, and to be able to swap between them in the mind with ease.