Thinking Functionally with Haskell (18 page)

How would you add 1 to every element in a given matrix of integers? How would you sum the elements of a matrix? The function
zipWith (+)
adds two rows, but what function would add two matrices? How would you define matrix multiplication?

Exercise B

What are the dimensions of the matrix
[[],[]]
? Of the matrix
[]
?

The function
cols
(here renamed as
transpose
) was defined by

transpose :: [[a]] -> [[a]]

transpose [xs]
= [[x] | x <- xs]

transpose (xs:xss) = zipWith (:) xs (transpose xss)

Fill in the dots that would enable you to replace the first clause by

transpose [] = ...

The above definition of
transpose
proceeds row by row. Here is part of a definition that proceeds column by column:
transpose xss = map head xss:transpose (map tail xss)

Complete this definition.

Exercise C

Which of the following equations are true (no justification is necessary):

Exercise D

Given a function
sort :: (Ord a) => [a] -> [a]
that sorts a list, construct a definition of
nodups :: (Ord a) => [a] -> Bool

Exercise E

The function
nub :: (Eq a) => [a] -> [a]
removes duplicates from a list (a version of this function is available in the library
Data.List
). Define
nub
. Assuming the order of the elements in the result is not important, define
nub :: (Ord a) => [a] -> [a]

so that the result is a more efficient function.

Exercise F

The functions
takeWhile
and
dropWhile
satisfy
span p xs = (takeWhile p xs,dropWhile p xs)

Give direct recursive definitions of
takeWhile
and
dropWhile
.

Assuming
whiteSpace :: Char -> Bool
is a test for whether a character is
white space (such as a space, a tab or a newline) or a visible character, construct a definition of
words :: String -> [Word]

that breaks a string up into a list of words.

Exercise G

Define
minimum :: Ord a => [a] -> a
.

Exercise H

Why didn’t we define
solve
By The Following?

Answer to Exercise A

Adding 1 to every matrix element is defined by
map (map (+1))
.

Summing a matrix is defined by
sum . map sum
, where
sum
sums a list of numbers. Alternatively, we could use
sum . concat
.

Matrix addition is defined by
zipWith (zipWith (+))
.

For matrix multiplication we first define

Then we have

Answer to Exercise B

The matrix
[[],[]]
has dimensions 2 × 0. The matrix
[]
has dimensions 0 ×
n
for every
n
. The transpose of such a matrix therefore has to have dimensions
n
× 0 for every
n
. The only reasonable possibility is to let
n
be infinite:

transpose :: [[a]] -> [[a]]

transpose []
= repeat []

transpose (xs:xss) = zipWith (:) xs (transpose xss)

where
repeat x
gives an infinite list of repetitions of
x
. Note that

transpose [xs] = zipWith (:) xs (repeat [])

= [[x] | x <- xs]

The alternative definition is

The assumption in the first line is that if the first row is empty, then all the rows are empty and the transpose is the empty matrix.

Answer to Exercise C

Both the equations are true.

Answer to Exercise D

Answer to Exercise E

The function
dropWhile
is defined in the next exercise.

Answer to Exercise F

Answer to Exercise G

minimum :: Ord a => [a] -> a

minimum [x]
= x

minimum (x:xs) = x `min` minimum xs

Note that the minimum of the empty list is undefined.

Answer to Exercise H

The suggested definition of
solve
would return the undefined value if the matrix becomes complete after one round of pruning.

The
Independent
newspaper no longer uses the rubric for Sudoku quoted at the start of the chapter. The presentation follows that in my book
Pearls of Functional Algorithm Design
(Cambridge, 2010). The site
haskell.org/haskellwiki/Sudoku

contains about 20 Haskell implementations of Sudoku, many of which use arrays and/or monads. We will meet arrays and monads in
Chapter 10
.

We have seen a lot of laws in the previous two chapters, though perhaps the word ‘law’ is a little inappropriate because it suggests something that is given to us from on high and which does not have to be proved. At least the word has the merit of being short. All of the laws we have encountered so far assert the equality of two functional expressions, possibly under subsidiary conditions; in other words, laws have been equations or
identities
between functions, and calculations have been point-free calculations (see
Chapter 4
, and the answer to Exercise K for more on the point-free style). Given suitable laws to work with, we can then use equational reasoning to prove other laws. Equational logic is a simple but powerful tool in functional programming because it can guide us to new and more efficient definitions of the functions and other values we have constructed. Efficiency is the subject of the following chapter. This one is about another aspect of equational reasoning, proof by induction. We will also show how to shorten proofs by introducing a number of
higher-order
functions that capture common patterns of computations. Instead of proving properties of similar functions over and over again, we can prove more general results about these higher-order functions, and appeal to them instead.

Consider the following definition of the exponential function:

exp :: Num a => a -> Nat -> a

exp x Zero = 1

exp x (Succ n) = x * exp x n

In the old days we could have written

exp :: Num a => a -> Int -> a
exp x 0 = 1

exp x (n+1) = x * exp x n

but this precise form of definition using a
(n+1)
-pattern is no longer allowed in the current standard version of Haskell, Haskell 2010.

Anyway, we would expect that the equation

exp x (m+n) = exp x m * exp x n

is true for all
m
and
n
. After all,
x
^m
+
n
=
x
^m
x
ⁿ
is a true equation of mathematics. But how can we prove this
law?

The answer, of course, is by
induction
. Every natural number is either
Zero
or of the form
Succ n
for some natural number
n
. That is exactly what the definition
data Nat = Zero | Succ Nat

of the data type
Nat
tells us. So to prove that
P
(
n
) holds for all natural numbers
n
, we can prove 1.
P
(0) holds;

2. For all natural numbers
n
, that
P
(
n
+ 1) holds assuming that
P
(
n
) does.

We have reverted to writing 0 for
Zero
and
n
+1 for
Succ n
, and we shall continue to do so. In the second proof we can assume
P
(
n
) and use this assumption to prove
P
(
n
+ 1).

As an example we prove that

exp x (m+n) = exp x m * exp x n

for all
x
,
m
and
n
by induction on
m
. We could also prove it by induction on
n
but that turns out to be more complicated. Here is the proof:
Case
0

exp x (0 + n)
exp x 0 * exp x n

=
{since
0 + n = n
}
=
{
exp.1
}

exp x n
1 * exp x n

=
{since
1 * x = x
}

exp x n

Case
m+1

exp x ((m + 1) + n))
exp x (m+1) * exp x n
=
{arithmetic}
=
{
exp.2
}

exp x ((m + n) + 1
(x
exp x m)
exp x n
=
{
exp.2
}
=
{since
*
is associative}

x * exp x (m + n)
x
(exp x m
exp x n)
=
{induction}

x
(exp x m
exp x n)

The above format will be used in all induction proofs. The proof breaks into two cases, the
base case
0 and the
inductive case n
+ 1. Each case is laid out in two columns, one for the left-hand side of the equation, and one for the right-hand side. (When there is not enough space for two columns, we display one after the other.) Each side is simplified until one can go no further, and the proof of each case is completed by observing that each side simplifies to the same result. The hints
exp.1
and
exp.2
refer to the first and second equations defining
exp
.

Finally, observe that the proof depends on three further laws, namely that

(m + 1) + n = (m + n) + 1

1 * x
= x

(x * y)
z = x
(y * z)

If we were recreating all of arithmetic from scratch – and that would be a tedious thing to do – we would also have to prove these laws. In fact, only the first can be proved because it is entirely about natural numbers and we have defined the operation of addition on natural numbers. The second two rely on the implementation of multiplication prescribed by Haskell for the various instances of the type class
Num
.

In fact, the associative law breaks down for floating-point numbers:

ghci> (9.9e10 * 0.5e-10) * 0.1e-10 :: Float

4.95e-11

ghci> 9.9e10 * (0.5e-10 * 0.1e-10) :: Float

4.9499998e-11

Recall that in scientific notation
9.9e10
means
9.9 * 10^10
. So, although our proof was correct mathematically, one of the provisos in it wasn’t, at least in Haskell.

We have seen that every finite list is either the empty list
[]
or of the form
x:xs
where
xs
is a finite list. Hence, to prove that
P
(
xs
) holds for all finite lists
xs
, we can prove: 1.
P
(
[]
) holds;

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

As an example, recall the definition of concatenation
(++)
:
[] ++ ys = ys