25.1 Chapter Introduction

The goal of this chapter is to show how to state and prove Haskell “laws”.

This chapter depends upon the reader understanding Haskell’s polymorphic, higher-order list programming concepts (e.g., from Chapters 4-5, 8-9, and 13-17), but it is otherwise independent of other preceding chapters.

The chapter provides useful tools that can be used in stating and formally proving function and module contracts (Chapters 6, 7, and 22) and type class laws (Chapter 23). It supports reasoning about program generalization (Chapter 19) and type inference (Chapter 24).

The following two chapters on program synthesis (Chapters 26 and 27) build on the concepts and techniques introduced by this chapter.

25.2 Referential Transparency Revisited

Referential transparency is probably the most important property of purely functional programming languages like Haskell.

Chapter 2 defines referential transparency to mean that, within some well-defined context, a variable (or other symbol) always represents the same value. This allows one expression to be replaced by an equivalent expression or, more informally, “equals to be replaced by equals”.

Chapter 8 shows how referential transparency underpins the evaluation (i.e., substitution or reduction) model for Haskell and similar functional languages.

In this chapter, we see that referential transparency allows us to state and prove various “laws” or identities that hold for functions and to use these “laws” to transform programs into equivalent ones. Referential transparency underlies how we reason about Haskell programs.

25.3 Stating and Proving Laws

As a purely functional programming language, Haskell supports mathematical reasoning mostly within the programming language itself. We can state properties of functions and prove them using a primarily equational, or calculational, style of proof. The proof style is similar to that of high school trigonometric identities.

    infixr 5 ++

    (++) :: [a] -> [a] -> [a] 
    [] ++ xs     = xs            -- append.1 
    (x:xs) ++ ys = x:(xs ++ ys)  -- append.2

25.4 Example: Relating length and ++

Suppose that the list length function is defined as follows (from Chapter 13}).

    length :: [a] -> Int 
    length []     =  0              -- length.1 
    length (_:xs) =  1 + length xs  -- length.2

Prove:

For all finite lists xs and ys:

length (xs++ys) = length xs + length ys.

Proof:

Because of the way ++ is defined, we choose xs as the induction variable.

Base case xs = []:

length [] + length ys

$=$ { length.1 (left to right) }

0 + length ys

$=$ { 0 is identity for addition }

length ys

$=$ { append.1 (right to left) }

length ([] ++ ys)

This establishes the base case.

Inductive case xs = (a:as):

Assume length (as ++ ys) = length as + length ys;
prove length ((a:as) ++ ys) = length (a:as) + length ys.

length ((a:as) ++ ys)

$=$ { append.2 (left to right) }

length (a:(as ++ ys))

$=$ { length.2 (left to right) }

1 + length (as ++ ys)

$=$ { induction hypothesis }

1 + (length as + length ys)

$=$ { associativity of addition }

(1 + length as) + length ys

$=$ { length.2 (right to left, value of a arbitrary) }

length (a:as) + length ys

This establishes the inductive case.

Therefore, length (xs ++ ys) = length xs + length ys. Q.E.D.

Note: The proof above uses the associativity and identity properties of integer addition.

25.5 Example: Relating take and drop

Remember the definitions for the list functions take and drop from Chapter 13}.

    take :: Int -> [a] -> [a]
    take n _ | n <= 0 = []                -- take.1
    take _ []         = []                -- take.2
    take n (x:xs)     = x : take (n-1) xs -- take.3

    drop :: Int -> [a] -> [a] 
    drop n xs | n <= 0 = xs               -- drop.1
    drop _ []          = []               -- drop.2
    drop n (_:xs)      = drop (n-1) xs    -- drop.3

Prove:

For any natural numbers n and finite lists xs,

take n xs ++ drop n xs = xs.

Proof:

Note that both take and drop use both arguments to distinguish the cases. Thus we must do an induction over all natural numbers n and all finite lists xs.

We would expect four cases to consider, the combinations from n being zero and nonzero and xs being nil and non-nil. But an examination of the definitions for the functions reveal that the cases for n = 0 collapse into a single case.

Base case n = 0:

take 0 xs ++ drop 0 xs

$=$ { take.1, drop.1 (both left to right) }

[] ++ xs

$=$ { ++ identity xs }

xs

This establishes the case.

Base case n = m+1, xs = []:

take (m+1) [] ++ drop (m+1) []

$=$ { take.2, drop.2 (both left to right) }

[] ++ []

$=$ { ++ identity }

[]

This establishes the case.

Inductive case n = m+1, xs = (a:as):

Assume take m as ++ drop m as = as;
prove take (m+1) (a:as) ++ drop (m+1) (a:as) = (a:as).

take (m+1) (a:as) ++ drop (m+1) (a:as)

$=$ { take.3, drop.3 (both left to right) }

(a:(take m as)) ++ drop m as

$=$ { append.2 (left to right) }

a:(take m as ++ drop m as)

$=$ { induction hypothesis }

(a:as)

This establishes the case.

Therefore, the property is proved. Q.E.D.

25.6 Example: Equivalence of Functions

What do we mean when we say two functions are equivalent?

Usually, we mean that the “same inputs” yield the “same outputs”. For example, single argument functions f and g are equivalent if f x $=$ g x for all x.

In Chapter 14. we defined two versions of a function to reverse the elements of a list. Function rev uses backward recursion and function reverse (called reverse' in Chapter 14) uses a forward recursive auxiliary function rev'.

    rev :: [a] -> [a] 
    rev []      =  []                          -- rev.1 
    rev (x:xs)  =  rev xs ++ [x]               -- rev.2 

    reverse :: [a] -> [a] 
    reverse xs  =  rev' xs []                  -- reverse.1 
        where rev' [] ys     = ys              -- reverse.2 
              rev' (x:xs) ys = rev' xs (x:ys)  -- reverse.3 

To show rev and reverse are equivalent, we must prove that, for all finite lists xs:

    rev xs = reverse xs

If we unfold (i.e., simplify) reverse one step, we see that we need to prove:

    rev xs = rev' xs []

Thus let’s try to prove this by structural induction on xs.

Base case xs = []:

rev []

$=$ { rev.1 (left to right) }

[]

$=$ { reverse.2 (right to left) }

rev' [] []

This establishes the base case.

Inductive case xs = (a:as):

Assume rev as = rev' as []; prove rev (a:as) = rev' (a:as) [].

First, we simplify the left side.

rev (a:as)

$=$ { rev.2 (left to right) }

rev as ++ [a]

Then, we simplify the right side.

rev' (a:as) []

$=$ { reverse.3 (left to right) }

rev' as [a]

Thus we need to show that rev as ++ [a] = rev' as [a]. But we do not know how to proceed from this point.

Maybe another induction. But that would probably just bring us back to a point like this again. We are stuck!

Let’s look back at rev xs = rev' xs []. This is difficult to prove directly. Note the asymmetry, one argument for rev versus two for rev'.

Thus let’s look for a new, more symmetrical, problem that might be easier to solve. Often it is easier to find a solution to a problem that is symmetrical than one which is not.

Note the place we got stuck above (proving rev as ++ [a] = rev' as [a]) and also note the equation reverse.3. Taking advantage of the identity element for ++, we can restate our property in a more symmetrical way as follows:

rev xs ++ [] = rev' xs []

Note that the constant [] appears on both sides of the above equation. We can now apply the following generalization heuristic [8,13]. (That is, we try to solve a “harder” problem.)

Heuristic:

Replace constant by variable

That is, generalize by replacing a constant (or any subexpression) by a new variable.

Thus we try to prove the more general proposition:

    rev xs ++ ys = rev' xs ys

The case ys = [] gives us what we really want to hold. Intuitively, this new proposition seems to hold. Now let’s prove it formally. Again we try structural induction on xs.

Base case xs = []:

rev [] ++ ys

$=$ { rev.1 (left to right) }

[] ++ ys

$=$ { append.1 (left to right) }

ys

$=$ { reverse.2 (right to left) }

rev' [] ys

This establishes the base case.

Inductive case xs = (a:as):

Assume rev as ++ ys = rev' as ys for any finite list ys;  prove rev (a:as) ++ ys = rev' (a:as) ys.

rev (a:as) ++ ys

$=$ { rev.2 (left to right) }

(rev as ++ [a]) ++ ys

$=$ { ++ associativity, Note 1 }

rev as ++ ([a] ++ ys)

$=$ { singleton law, Note 2 }

rev as ++ (a:ys)

$=$ { induction hypothesis }

rev' as (a:ys)

$=$ { reverse.3 (right to left) }

rev' (a:as) ys

This establishes the inductive case.

Notes:

1. We could apply the induction hypothesis here, but it does not seem profitable. Keeping the expressions in terms of rev and ++ as long as possible seems better; we know more about those expressions.

2. The singleton law is [x] ++ xs = x:xs for any element x and finite list xs of the same type. Proof of this is left as an exercise for the reader.

Therefore, we have proved rev xs ++ ys = rev' xs ys and, hence:

    rev xs = reverse xs

The key to the performance improvement here is the solution of a “harder” problem: function rev' does both the reversing and appending of a list while rev separates the two actions.

25.7 What Next?

This chapter illustrated how to state and prove Haskell “laws” about already defined functions.

Chapters 26} and 27} on program synthesis illustrate how to use similar reasoning methods to synthesize (i.e., derive or calculate) function definitions from their specifications.

25.8 Exercises

This set of exercises uses functions defined in this and previous chapters including the following:

• Functions map, filter, foldr, foldl, and concatMap are defined in Chapter 15.

• Functional composition, identity combinator id, and function all are defined in Chapter 16}.

• Functions takeWhile and dropWhile are defined in Chapter 17.

Prove the following properties using the proof methods illustrated in this chapter.

1. Prove for all x of some type and finite lists xs of the same type (i.e., the singleton law):

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

2. Consider the definition for length given in the text of this chapter and the following definition for len:

       len :: Int -> [a] -> Int 
       len n [ ]    = n             -- len.1 
       len n (_:xs) = len (n+1) xs  -- len.2

   Prove for any finite list xs: len 0 xs = length xs.

3. Prove for all finite lists xs and ys of the same type:

       reverse (xs ++ ys)  =  reverse ys ++ reverse xs

   Hint: The function reverse (calledreverse' in Chapter 14.) uses forward recursion. Backward recursive definitions are generally easier to use in inductive proofs. In Chapter 14., we also defined a backward recursive function rev and proved that rev xs = reverse xs for all finite lists xs. Thus, you may find it easier to substitute rev for reverse and instead prove:

       rev (xs ++ ys)  =  rev ys ++ rev xs

4. Prove for all finite lists xs of some type:

       reverse (reverse xs)  =  xs

5. Prove for all natural numbers m and n and all finite lists xs:

       drop n (drop m xs)  =  drop (m+n) xs

6. Consider the rational number package from Chapter 7.. Prove for any Rat value r that satisfied the interface invariant for the abstract module RationalRep:

       addRat r zeroRat  =  r  =  addRat zeroRat r

7. Consider the two definitions for the Fibonacci function in Chapter 9. Prove for any natural number n:

       fib n  =  fib' n

   Hint: First prove, for n $\geq$ 2:

       fib'' n p q = fib'' (n-2) p q + fib'' (n-1) p q

8. Prove that the id function is the identity element for functional composition. That is, for any function f :: a -> b, prove:

       f . id  =  f  =  id . f

9. Prove that functional composition is associative. That is, for any function f :: a -> a, g :: a -> a, and h :: a -> a, prove:

       (f . g) . h  =  f . (g . h)

10. Prove for all finite lists xs and ys of the same type and function f on that type:

        map f (xs ++ ys)  =  map f xs ++ map f ys

11. Prove for all finite lists xs and ys of the same type and predicate p on that type:

       filter p (xs ++ ys)  =  filter p xs ++ filter p ys

12. Prove for all finite lists xs and ys of the same type and all predicates p on that type:

        all p (xs ++ ys)  =  (all p xs) && (all p ys)

    The definition for && is as follows:

        (&&) :: Bool -> Bool -> Bool 
        False && x = False  -- second argument not evaluated 
        True  && x = x      -- second argument returned

13. Prove for all finite lists xs of some type and predicates p and q on that type:

        filter p (filter q xs)  =  filter q (filter p xs)

14. Prove for all finite lists xs and ys of the same type and for all functions f and values a of compatible types:

        foldr f a (xs ++ ys)  =  foldr f (foldr f a ys) xs

15. Prove for all finite lists xs of some type and all functions f and g of conforming types:

        map (f . g) xs  =  (map f . map g) xs

16. Prove for all finite lists of finite lists xss of some base type and function f on that type:

        map f (concat xss)  =  concat (map (map f) xss)

17. Prove for all finite lists xs of some type and functions f on that type:

        map f xs  =  foldr ((:) .f) [] xs

18. Prove for all lists xs and predicates p on the same type:

        takeWhile p xs ++ dropWhile p xs  =  xs

19. Prove that, if *** is an associative binary operation of type t -> t with identity element z (i.e., a monoid), then:

        foldr (***) z xs  =  foldl (***) z xs

20. Consider the Haskell type for the natural numbers given in an exercise in Chapter 21.

        data Nat = Zero | Succ Nat

    For the functions defined in that exercise, prove the following:

    1. Prove that intToNat and natToInt are inverses of each other.

    2. Prove that Zero is the (right and left) identity element for addNat.

    3. Prove for any Nats x and y:

           addNat (Succ x) y  =  addNat x (Succ y)

    4. Prove associativity of addition on Nat’s. That is, for any Nats x, y, and z:

           addNat x (addNat y z)  =  addNat (addNat x y) z

    5. Prove commutativity of addition on Nat’s. That is, for any Nats x and y:

           addNat x y  =  addNat y x

25.9 Acknowledgements

In Summer 2018, I adapted and revised this chapter from Chapter 11 of my Notes on Functional Programming with Haskell [9].

These previous notes drew on the presentations in the first edition of the classic Bird and Wadler textbook [3] and other functional programming sources [1,2,15,17,18]. They were also influenced by my research, study, and teaching related to program specification, verification, derivation, and semantics [[4]; [5]; [6]; [7]; [8]; [10]; [11]; [12]; [13]; [14]; [16]; vanGesteren1990].

I incorporated this work as new Chapter 25, Proving Haskell Laws, in the 2018 version of the textbook Exploring Languages with Interpreters and Functional Programming and continue to revise it.

I retired from the full-time faculty in May 2019. As one of my

post-retirement projects, I am continuing work on this textbook. In January 2022, I began refining the existing content, integrating additional separately developed materials, reformatting the document (e.g., using CSS), constructing a bibliography (e.g., using citeproc), and improving the build workflow and use of Pandoc.

I maintain this chapter as text in Pandoc’s dialect of Markdown using embedded LaTeX markup for the mathematical formulas and then translate the document to HTML, PDF, and other forms as needed.

25.10 Terms and Concepts

Referential transparency, equational reasoning, laws, definition, simplification, calculation, associativity, identity, monoid, singleton law, equivalence of functions.

25.11 References