Equational Reasoning

EquationalReasoning.md

Overview

One of the benefits of functional programming is that it's much simpler to figure out how your code will run. Because functional languages are based on math, you're really definining functions in terms of equality. As such, you can substitute terms for one another. In this example, I'll use Haskell, because the syntax highlights this point, but the principle applies in multiple languages (Erlang, Elixir, OCaml, etc).

In Haskell, when you write x = 5 that means that x and 5 are the same thing. As such, whereever you have an x in your program, you can replace it with 5, or vice-versa. Because x and 5 are the same, these substitutions don't break your program. This ability to substitute terms for one another is called equational reasoning.

In fact, this is how Haskell runs your program — it repeatedly applies substitutions until it has one giant main function.

I'm going to work through a short example using linked lists.

List Definitions

We define a list this way in Haskell:

data [] a = [] | a : [a]

This says that a list is either empty, [], or non-empty, written as a : [a]. The colon, :, is pronounced "cons" because it constructs new lists. You can think of a non-empty list as a value, a, glued to the front of another list, which is called the tail.

The critical aspect to this definition is that it's recursive -- the tail of a non-emtpy list is itself a list.

We can look at lists in the Haskell REPL:

% ghci
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/derek/.ghci
λ> let list1 = [1,2,3] -- this is the shorthand syntax for a list
λ> let list2 = 1 : 2 : 3 : [] -- this is the long-hand version.
λ> list1 == list2
True

In the example above, list2 is a non-empty list. Its head is 1, and its tail is the non-empty list 2:3:[].

List Operations

When we define functions that operate on lists, we need to handle both cases (an empty list and non-empty list). For example, let's look at length:

length :: [a] -> Int
length []          = 0                -- pattern for an empty list
length (head:tail) = 1 + length tail  -- pattern for a non-empty list

To explain this syntax:

The first line, length :: [a] -> Int, is the function declaration -- it tells Haskell the number and types of the inputs and outputs. It's roughly equivalent to the def declaration in Ruby. In this case the length function get a list of things -- that's the [a] part -- and returns an Int.

Next we have two patterns, one for an empty list and one for a non-empty list.

For an empty list, length [] = 0, we're saying that the length of an empty list is zero. That's not too surprising.

The second pattern is for a non-empty list. Remember from above that a non-empty list has a head and a tail. We use pattern matching -- the (head:tail) part -- to split the list apart into two variables, called head and tail. So at this point, we know that we have one element, the head, and another list, the tail. We don't know anything about tail other than that it's a list. It could be empty, or it could have a million elements in it. But we definitely know that we have at least one thing, the head, so we can say that the length is one plus the length of the tail.

Example

Let's walk through how we compute length [1,2,3].

The length function has two patterns, so we need to decide which to apply. The list [1,2,3] isn't empty, so we apply the second pattern. This gives us two variables: head, which is 1, and tail, which is [2,3]. Next we substitute the right hand side for the left. We have this equation:

length [1,2,3] = 1 + length [2,3] -- equation A

Now we have a new expression to evaluate, length [2,3]. We apply the same algorithm as above. The length function has two pattern, so we need to decide which to apply. The list [2,3] isn't empty, so we apply the second pattern. So the head is 2 and the tail is [3]. Next we substitute the right hand side for the left. This tell us that length [2,3] is 1 + length [3]. Plugging that substitution into equation A, we get:

length [1,2,3] = 1 + 1 + length [3] -- equation B

Now we have a new expression to evaluate, length [3]. The length function has two pattern, so we need to decide which to apply. The list [3] isn't empty, so we apply the second pattern. So the head is 3 and the tail is []. Next we substitute the right hand side for the left. This tells us that length [3] is 1 + length []. Plugging that substitution into equation B we get:

length [1,2,3] = 1 + 1 + 1 + length [] -- equation C

Now we have a new expression to evaluate, length []. The length function has two pattern, so we need to decide which to apply. The list [] is empty, so we apply the first pattern. Next we substitute the right hand side for the left. This tell us that length [] is 0. Plugging that substitution into equation C we get:

length [1,2,3] = 1 + 1 + 1 + 0 -- equation D

At this point we can evaluate the right hand side. 1+1+1+0 is 3. Plugging that substitution into equation D, we get:

length [1,2,3] = 3

This is an incredibly common pattern in functional languages. We have a list of things, and we need to process it. We know that a list is either empty or non-empty. We defined a base case for the empty list, and a derived case for non-empty lists that pops off the head element, does something with it, and recursively calls itself on the tail.