Thinking Functionally with Haskell (38 page)

primes
₄
=
2 : 3 : 5 : 7 : · · · : 47 :⊥

What list does
primes
₅
produce?

Exercise J

Another way of generating the primes is known as the
Sieve of Sundaram
, after its discoverer S.P. Sundaram in 1934:

primes = 2:[2*n+1 | n <- [1..] \\ sundaram]

sundaram = mergeAll [[i+j+2*i*j | j <- [i..]] | i <- [1..]]

To show that the list comprehension in the definition of
primes
generates exactly the odd primes, it is sufficient to prove that the term
2*n+1
is never composite, which is to say that it never factorises into
(2*i+1)*(2*j+1)
for positive integers
i
and
j
. Why is this so?

Exercise K

Is the function
f
, defined by
f
(⊥) =0 and
f
(
x
) =1 for
x
≠⊥, computable? How about the function that returns ⊥ on all finite or partial lists, and 1 on all infinite lists?

Exercise L

By definition, a
torus
is a doubly-cyclic, doubly-doubly-linked list. It is a cyclic doubly-linked list in the left/right direction, and also in the up/down direction. Given a matrix represented as a list of length
m
of lists, all of length
n
, construct a definition of
mkTorus :: Matrix a -> Torus a

where

That looks tricky, but the answer is short enough to be tweeted.

Answer to Exercise A

No, since
foldl1 f xs = undefined
for any infinite list
xs
.

Answer to Exercise B

The definition is

Note that if
xs
is infinite, then
xs ++ ys
=
xs
, so
cycle
is the identity function on infinite lists.

Answer to Exercise C

The one-liner is:

Answer to Exercise D

Answer to Exercise E

The proof of
approx n xs
⊑
xs
is by induction on
n
. The base case is easy but the induction step involves a sub-induction over
xs
. The base cases (the empty list and the undefined list) of the sub-induction are easy and the inductive case is

approx (n+1) (x:xs)

=
{definition}

x:approx n xs

⊑ {induction and monotonicity of
(x:)
}

x:xs
.

The proof of

(∀
n
:
approx n xs
⊑
ys
) ⇒
xs
⊑
ys
is by induction on
xs
. The claim is immediate for the undefined and empty lists, and for the inductive case we have (∀
n
:
approx n (x:xs)
⊑
ys
) ⇒
xs
⊑
head ys
∧ (∀
n
:
approx n xs
⊑
tail ys
) by the definitions of
approx
and the approximation ordering on lists. By induction we therefore have
x:xs
⊑
head ys:tail ys
=
ys
.

It follows that

by the definition of limit.

Answer to Exercise F

The two lists
repeat undefined
and
undefined
are not equal, but
(repeat undefined)!!n = undefined!!n

for all
n
because both sides are ⊥.

Answer to Exercise G

We have to show that

approx n (iterate f x) = approx n (x:map f (iterate f x))

for all natural numbers
n
. This claim follows from

approx n (iterate f (f x))

= approx n (map f (iterate f x))

which we establish by induction on
n
. For the inductive step we simplify each side. For the left-hand side:

approx (n+1) (iterate f (f x))

=
{definition of
iterate
}

approx (n+1) (f x:iterate f (f (f x)))

=
{definition of
approx
}

f x: approx n (iterate f (f (f x)))

=
{induction}

f x: approx n (map f (iterate f (f x)))

For the right-hand side:

approx (n+1) (map f (iterate f x))

=
{definition of
iterate
and
map
}

approx (n+1) (f x:map f (iterate f (f x)))

=
{definition of
approx
}

f x: approx n (map f (iterate f (f x)))

Answer to Exercise H

Yes, since

foldr xmerge [] (xs:undefined) = xmerge xs undefined

and the right-hand side begins with the first element of
xs
.

Answer to Exercise I

The proof is by induction. We have first to show that
crs (n+1)
is the result of merging
c
₁
:
c
²
: · · ·
c
_m
:⊥, where
with the infinite list of multiples
p
_n
+1
p
_n
+1
,
p
_n
+1
(
p
_n
+1
+1), . . . of
p
_n
+1
. That gives the partial list of all composite numbers up to
Finally, we need the result that
The partial list
primes
₅
produces all the primes smaller than 2209 = 47 × 47.

Answer to Exercise J

Because an odd integer is excluded from the final list if it takes the form 2
n
+ 1 where
n
is of the form
i
+
j
+2
ij
. But 2(
i
+
j
+2
ij
)+1 =(2
i
+1)(2
j
+1).

Answer to Exercise K

No,
f
is not monotonic: ⊥⊑ 1 but
f
(⊥) ⋢
f
(1). For the second function (call it
g
) we have
xs
⊑
ys
implies
g
(
xs
) ⊑
g
(
ys
), so
g
is monotonic. But
g
is not continuous, so it’s not computable.

Answer to Exercise L

The definition is

Whereas
rotr
and
rotl
rotate the rows of a matrix,
map rotr
and
map rotl
rotate the columns. The definition of
zipWith5
has to be made non-strict in its last four arguments.

Melissa O’Neill has written a nice pearl on sieve methods for generating primes; see ‘The genuine sieve of Eratosthenes’,
Journal of Functional Programming
19 (1), 95–106, 2009. Ben Sijtsma’s thesis
Verification and derivation of infinite-list programs
(University of Groningen, the Netherlands, 1988) studies various aspects of infinite-list programs and gives a number of techniques for reasoning about them. One chapter is devoted to the proof of fairness in the paper–rock–scissors game.

My paper, ‘On building cyclic and shared data structures in Haskell’,
Formal Aspects of Computing
24(4–6), 609–621, July 2012, contains more examples of the uses of infinite and cyclic lists. See also the article on ‘Tying the knot’ at
haskell.org/haskellwiki/Tying_the_Knot

Hamming’s problem has been used as an illustration of cyclic programs since the early days of functional programming.

Back in
Chapter 2
we described the function
putStrLn
as being a Haskell
command
, and
IO a
as being the type of input–output
computations
that interact with the outside world and deliver values of type
a
. We also mentioned some syntax, called
do
-notation
, for sequencing commands. This chapter explores what is really meant by these words, and introduces a new style of programming called
monadic
programming. Monadic programs provide a simple and attractive way to describe interaction with the outside world, but are also capable of much more: they provide a simple sequencing mechanism for solving a range of problems, including exception handling, destructive array updates, parsing and state-based computation. In a very real sense, a monadic style enables us to write functional programs that mimic the kind of imperative programs one finds in languages such as Python or C.

The type
IO a
is an abstract type in the sense described in the previous chapter, so we are not told how its values, which are called
actions
or commands, are represented. But you can think of this type as being
type IO a = World -> (a,World)