Thinking Functionally with Haskell (19 page)

(x:xs) ++ ys = x : (xs ++ ys)

We prove that
++
is associative:

(xs ++ ys) ++ zs = xs ++ (ys ++ zs)

for all finite lists
xs
and for all lists
ys
and
zs
(note that neither of the last two is required to be a finite list), by induction on
xs
:
Case
[]

([] ++ ys) ++
zs [] ++ (ys ++ zs)
=
{
++.1
}
=
{
++.1
}

ys ++ zs
ys ++ zs

Case
x:xs

((x:xs) ++ ys) ++ zs
(x:xs) ++ (ys ++ zs)
=
{
++.2
}
=
{
++.2
}

(x:(xs ++ ys)) ++ zs
x:(xs ++ (ys ++ zs))
=
{
++.2
}
=
{induction}

x:((xs ++ ys) ++ zs)
x:((xs ++ ys) ++ zs)
As another example, given the definition

reverse []
= []

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

We prove that
reverse
is an involution:

reverse (reverse xs) = xs

for all finite lists
xs
. The base case is easy and the inductive case proceeds:
Case
x:xs

reverse (reverse (x:xs))

=
{
reverse.2
}

reverse (reverse xs ++ [x])

=
{????}

x:reverse (reverse xs)

=
{induction}

x:xs

The right-hand column is omitted in this example, since it consists solely of
x:xs
. But we got stuck in the proof halfway through. We need an auxiliary result, namely that
reverse (ys ++ [x]) = x:reverse ys

for all finite lists
ys
. This auxiliary result is also proved by induction:
Case
[]

reverse ([] ++ [x])
x:reverse []

=
{
++.1
}
=
{
reverse.1
}

reverse [x]
[x]

=
{
reverse.2
}

reverse [] ++ [x]

=
{
reverse.1
and
++.1
}

[x]

Case
y:ys

reverse ((y:ys) ++ [x])
x:reverse (y:ys)
=
{
++.2
}
=
{
reverse.2
}

reverse (y:(ys ++ [x]))
x:(reverse ys ++ [y])
=
{
reverse.2
}

reverse (ys ++ [x]) ++ [y]

=
{induction}

(x:reverse ys) ++ [y]

=
{
++.2
}

x:(reverse ys ++ [y])

The auxiliary result holds, and therefore so does the main result.

Induction over partial lists

Every partial list is either the undefined list or of the form
x:xs
for some
x
and some partial list
xs
. Hence, to prove that
P
(
xs
) holds for all partial lists
xs
we can prove that 1.
P
(
undefined
) holds;

2.
P
(
x:xs
) holds assuming
P
(
xs
) does, for all
x
and all partial lists
xs
.

As an example, we prove that

xs ++ ys = xs

for all partial lists
xs
and all lists
ys
:
Case
undefined

undefined ++ ys

=
{
++.0
}

undefined

Case
x:xs

(x:xs) ++ ys

=
{
++.2
}

x:(xs ++ ys)

=
{induction}

x:xs

In each case the trivial right-hand column is omitted. The hint
(++).0
refers to the failing clause in the definition of
(++)
: since concatenation is defined by pattern matching on the left-hand argument, the result is undefined if the left-hand argument is.

Induction over infinite lists

Proving that something is true of all infinite lists requires a bit of background that we will elaborate on in a subsequent chapter. Basically an infinite list can
be thought of as the limit of a sequence of partial lists. For example,
[0..]
is the limit of the sequence
undefined, 0:undefined, 0:1:undefined, 0:1:2:undefined,

and so on. A property
P
is called
chain complete
if whenever
xs
₀
, xs
₁
,
. . . is a sequence of partial lists with limit
xs
, and
P
(
xs
^_n
) holds for all
n
, then
P
(
xs
) also holds.

In other words, if
P
is a chain complete property that holds for all partial lists (and possibly all finite lists too), then it holds for all infinite lists.

Many properties are chain complete; for instance:

• All equations
  e
  1 =
  e
  2, where
  e
  1 and
  e
  2 are Haskell expressions involving universally quantified free variables, are chain complete.
  
• If
  P
  and
  Q
  are chain complete, then so is their conjunction
  P
  ∧
  Q
  .
  

But inequalities
e
1 ≠
e
2 are not necessarily chain complete, and neither are properties involving existential quantification. For example, consider the assertion
drop n xs = undefined

for some integer
n
. This property is obviously true for all partial lists, and equally obviously not true for any infinite list.

Here is an example proof. Earlier we proved that

(xs ++ ys) ++ zs = xs ++ (ys ++ zs)

for all finite lists
xs
and for all lists
ys
and
zs
. We can extend this chain complete property to
all
lists
xs
by proving
Case
undefined

(undefined ++ ys) ++ zs
undefined ++ (ys ++ zs)
=
{
++.0
}
=
{
++.0
}

undefined ++ zs
undefined

=
{
++.0
}

undefined

Thus
++
is a truly associative operation on lists, independent of whether the lists are finite, partial or infinite.

But we have to be careful. Earlier we proved

reverse (reverse xs) = xs

for all finite lists
xs
. Can we extend this property to all lists by proving the following additional case?

Case
undefined

reverse (reverse undefined)

=
{
reverse.0
}

undefined

That goes through but something is wrong: as a Haskell equation we have

reverse (reverse xs) = undefined

for all partial lists
xs
. What did we miss?

The answer is that in proving the involution property of
reverse
we made use of an auxiliary result:
reverse (ys ++ [x]) = x:reverse ys

for all finite lists
ys
. This result is not true for all lists, indeed not true for any partial list
ys
.

It follows that
reverse . reverse
is not the identity function on lists, A functional equation
f = g
over lists asserts that
f xs = g xs
for
all
lists
xs
, finite, partial and infinite. If the equation is true only for finite lists, we have to say so explicitly.

All the following functions have a common pattern:

sum []
= 0

sum (x:xs)
= x + sum xs

concat []
= []

concat (xs:xss)
= xs ++ concat xss

filter p []
= []

filter p (x:xs)
= if p x then x:filter p xs
else filter p xs

map f []
= []

map f (x:xs)
= f x:map f xs

Similarly, the proofs by induction of the following laws all have a common pattern:
sum (xs ++ ys)
= sum xs + sum ys
concat (xss ++ yss)
= concat xss ++ concat yss
filter p (xs ++ ys)
= filter p xs ++ filter p ys
map f (xs ++ ys)
= map f xs ++ map f ys
Can we not ensure that the functions above are defined as instances of a more general function, and the laws above as instances of a more general law? That would save a lot of repetitive effort.

The function
foldr
(fold from the right) is defined by
foldr :: (a -> b -> b) -> b -> [a] -> b

foldr f e []
= e

foldr f e (x:xs) = f x (foldr f e xs)

To appreciate this definition, consider

foldr (@) e [x,y,z] = x @ (y @ (z @ e))

[x,y,z] = x : (y : (z : []))

In other words,
foldr (@) e
applied to a list replaces the empty list by
e
, and
(:)
by
(@)
and evaluates the result. The parentheses group from the right, whence the name.

It follows at once that
foldr (:) []
is the identity function on lists. Furthermore,
sum
= foldr (+) 0

concat
= foldr (++) []

filter p
= foldr (\x xs -> if p x then x:xs else xs) []

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

The following fact captures all the identities mentioned above:

foldr f e (xs ++ ys) = foldr f e xs @ foldr f e ys

for some operation
(@)
satisfying various properties. We prove this equation by induction on
xs
. Along the way, we discover what properties of
f
,
e
and
(@)
we need.

Case
[]

foldr f e ([] ++ ys)
foldr f e [] @ foldr f e ys
=
{
++.1
}
=
{
foldr.1
}

foldr f e ys
e @ foldr f e ys

Hence we need
e @ x = x
for all
x
.

Case
x:xs

foldr f e ((x:xs) ++ ys)

=
{
++.2
}

foldr f e (x:(xs ++ ys)

=
{
foldr.2
}

f x (foldr f e (xs ++ ys))

=
{induction}

f x (foldr f e xs @ foldr f e ys)

The right-hand side in this case simplifies to

f x (foldr f e xs) @ foldr f e ys

So, in summary, we require that

e @ x = x

f x (y @ z) = f x y @ z

for all
x
,
y
and
z
. In particular the two requirements are met if
f = (@)
and
(@)
is associative with identity
e
. That immediately proves
sum (xs ++ ys) = sum xs + sum ys

concat (xss ++ yss) = concat xss ++ concat yss

For the
map
law, we require that

[] ++ xs = xs

f x:(xs ++ ys) = (f x:ys) ++ ys

Both immediately follow from the definition of concatenation.

For the law of
filter
we require that

if p x then x:(ys ++ zs) else ys ++ zs

= (if p x then x:ys else ys) ++ zs

This is immediate from the definitions of concatenation and conditional expressions.

Fusion

The most important property of
foldr
is the
fusion law
, which asserts that
f . foldr g a = foldr h b

provided certain properties of the ingredients hold. As two simple examples,

double . sum
= foldr ((+) . double) 0

length . concat = foldr ((+) . length) 0

In fact, many of the laws we have seen already are instances of the fusion law for
foldr
. In a word, the fusion law is a ‘pre-packaged’ form of induction over lists.

To find out what properties we need, we carry out an induction proof of the fusion law. The law is expressed as a functional equation, so we have to show that it holds for all finite and all partial lists:
Case
undefined

f (foldr g a undefined)
foldr h b undefined
=
{
foldr.0
}
=
{
foldr.0
}