Thinking Functionally with Haskell (16 page)

If your nose is good at sniffing out inefficiencies, you might suspect that this oneliner is not the best possible, and you would be right. We will return to this point in
Section 7.3
, but let’s just say that a more efficient definition is

cp (xs:xss) = [x:ys | x <- xs, ys <- yss]

where yss = cp xss

This version guarantees that
cp xss
is computed just once.

Now, what is
cp []
? The answer is not
[]
but
[[]]
. To see why the first is wrong, consider a little calculation:

cp [xs] = cp (xs:[])

= [x:ys | x <- xs, ys <- cp []]

= [x:ys | x <- xs, ys <- []]

= []

In fact with
cp [] = []
we can show that
cp xss = []
for all lists
xss
. So that definition is clearly wrong. You can check that the second alternative,
[[]]
, does give what is wanted.

Summarising, we can define
cp
by

For example,

ghci> cp [[1],[2],[3]]

[[1,2,3]]

ghci> cp [[1,2],[],[4,5]]

[]

In the second example there is no possible choice from the middle list, so the empty list is returned.

But what about matrices and
expand
, which does the same thing on matrices as
cp
does on lists? You will have to think a bit before seeing that what is wanted is

expand :: Matrix [Digit] -> [Grid]

expand = cp . map cp

That looks a little cryptic, but
map cp
returns a list of all possible choices for each row, and so applying
cp
to the result installs each choice for the rows in all possible ways. The general type of the right-hand side is
cp . map cp :: [[[a]]] -> [[[a]]]

and the declared type of
expand
is just a restricted version of this type. Note that
expand
returns the empty list if any element in any row is the empty list.

Finally, a valid grid is one in which no row, column or box contains duplicates:

valid :: Grid -> Bool

valid g = all nodups (rows g) &&

all nodups (cols g) &&

all nodups (boxs g)

The prelude function
all
is defined by
all p = and . map p

Applied to a finite list
xs
the function
all p
returns
True
if all elements of
xs
satisfy
p
, and
False
otherwise. The function
nodups
can be defined by

nodups :: (Eq a) => [a] -> Bool

nodups
[] = True

nodups (x:xs) = all (/=x) xs && nodups xs

Evaluation of
nodups
on a list of length
n
takes time proportional to
n
²
. As an alternative we could sort the list and check that it is strictly increasing. Sorting can be done in time proportional to
n
log
n
steps. That seems a big saving over
n
²
. However, with
n
= 9, it is not clear that using an efficient sorting algorithm is worthwhile. What would you prefer: 2
n
²
steps or 100
n
log
_²
n
steps?

It remains to define
rows
,
cols
and
boxs
. If a matrix is given by a list of its rows, then
rows
is just the identity function on matrices:

rows :: Matrix a -> Matrix a

rows = id

The function
cols
computes the transpose of a matrix. Thus if a matrix consists of
m
rows, where each row has length
n
, the transpose is a list of
n
rows, where each row has length
m
. Assuming both
m
and
n
are not zero, we can define

cols :: Matrix a -> Matrix a

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

cols (xs:xss) = zipWith (:) xs (cols xss)

It is usual in matrix algebra to suppose that the matrix is nonempty, and that certainly suffices here, but it is interesting to consider what happens if we allow
m
or
n
to be zero. This point is taken up in the exercises.

The function
boxs
is a little more interesting. We give the definition first and explain it afterwards:

boxs :: Matrix a -> Matrix a

boxs = map ungroup . ungroup .

map cols .

group . map group

The function
group
splits a list into groups of three:
group :: [a] -> [[a]]

group [] = []

group xs = take 3 xs:group (drop 3 xs)

The function
ungroup
takes a grouped list and ungroups it:

ungroup :: [[a]] -> [a]

ungroup = concat

The action of
boxs
in the 4 × 4 case, when
group
splits a list into groups of two rather than three, is illustrated by the picture

Grouping produces a list of matrices; transposing each matrix and ungrouping yields the boxes, as a matrix whose rows are the boxes of the original matrix.

Observe that instead of thinking about matrices in terms of indices, and doing arithmetic on indices to identify the rows, columns and boxes, we have gone for definitions of these functions that treat the matrix as a complete entity in itself. This style has aptly been called
wholemeal programming
. Wholemeal programming is good for you: it helps to prevent a disease called indexitis, and encourages lawful program construction.

For example, here are three laws that are valid on Sudoku grids:

In other words, all three functions are involutions. The first two are valid on all matrices, and the third is valid on arbitrary
n
²
×
n
²
matrices (provided we change
the definition of
group
to group by
n
). Two are easy to prove, but one is more difficult. The difficult law is not the one about
boxs
, as you might expect, but the involution property of
cols
. Though it is intuitively obvious that transposing a matrix twice gets you back to the original matrix, proving it from the definition of
cols
is a little tricky and we won’t go into details, basically because we haven’t yet discussed the tools available to do the job.

By contrast, here is the proof of the involution property of
boxs
. The proof is by simple equational reasoning. It makes use of various laws, including the functor laws of
map
, the fact that
id
is the identity element of composition, and the facts that

ungroup . group = id

group . ungroup = id

The second equation is valid only on grouped lists, but that will be the case in the calculation to come.

We will talk through the proof rather than lay everything out in a long chain. The starting point is to use the definition of
boxs
to rewrite
boxs . boxs
:

map ungroup . ungroup . map cols . group . map group .

map ungroup . ungroup . map cols . group . map group

The middle expression
map group . map ungroup
simplifies to
id
using the functor law of
map
and the property that
group
and
ungroup
are inverses. That gives

map ungroup . ungroup . map cols . group .

ungroup . map cols . group . map group

An appeal to
group . ungroup = id
gets us to

The functor law of
map
and the involution property of
cols
now gets us to
map ungroup . ungroup . group . map group

And the proof is finished off using
ungroup . group = id
twice more. As you can see, it’s a very simple calculation.

Here are three more laws, valid on
N
²
×
N
²
matrices of choices:
map rows . expand = expand . rows

map cols . expand = expand . cols

map boxs . expand = expand . boxs

We will make use of these laws in a short while.

Finally, here are two laws about
cp
:

The first law, a naturality law, is suggested solely by the type of
cp
; we saw similar laws in the previous chapter. The second law says that as an alternative to taking the cartesian product of a list of lists, and then retaining only those lists all of whose elements satisfy
p
, we can first filter the original lists to retain only those elements that satisfy
p
and then take the cartesian product. As the previous sentence illustrates, one equation can be worth a thousand words.

Summarising what we have at the moment,

Though executable in theory, this definition of
solve
is hopeless in practice. Assuming about 20 of the 81 entries are fixed initially, there are about 9
⁶¹
, or
ghci> 9^61

16173092699229880893718618465586445357583280647840659957609

grids to check! We therefore need a better approach.

To make a more efficient solver, an obvious idea is to remove any choices from a cell
c
that already occur as singleton entries in the row, column and box containing
c
. A singleton entry corresponds to a fixed choice. We therefore seek a function
prune :: Matrix [Digit] -> Matrix [Digit]

so that

filter valid . expand = filter valid . expand . prune

How can we define
prune
? Well, since a matrix is a list of rows, a good place to start is by pruning a single row. The function
pruneRow
is defined by

pruneRow :: Row [Digit] -> Row [Digit]

pruneRow row = map (remove fixed) row

where fixed = [d | [d] <- row]

The fixed choices are the singleton entries in each row. The definition of
fixed
uses a list comprehension involving a pattern: all elements of
row
that are not singletons are discarded.

The function
remove
removes the fixed choices from any choice that is not fixed:
remove :: [Digit] -> [Digit] -> [Digit]

remove ds [x] = [x]

remove ds xs
= filter (`notElem` ds) xs
The standard prelude function
notElem
is defined by

notElem :: (Eq a) => a -> [a] -> Bool

notElem x xs = all (/= x) xs

Here are a couple of examples of the use of
pruneRow
:
ghci> pruneRow [[6],[1,2],[3],[1,3,4],[5,6]]

[[6],[1,2],[3],[1,4],[5]]

ghci> pruneRow [[6],[3,6],[3],[1,3,4],[4]]

[[6],[],[3],[1],[4]]

In the first example,
[6]
and
[3]
are the fixed choices; removing these choices from the other entries reduces the last entry to a fixed choice. In the second example, removing the fixed choices reduces the second entry to the empty list of choices.

The function
pruneRow
satisfies the equation

filter nodups . cp = filter nodups . cp . pruneRow

In words, this equation says that pruning a row will not throw away any list that contains no duplicates. We will also make use of this law in a short while.

We are now nearly ready for a calculation that will determine the function
prune
. Nearly, but not quite because we are going to need two more laws: If
f . f = id
, then