Thinking Functionally with Haskell (21 page)

where
tails
is dual to
inits
and returns all the tail segments of a list:
tails :: [a] -> [[a]]

tails []
= [[]]

tails (x:xs) = (x:xs):tails xs

The definition of
segments
describes the process of taking all the initial segments of all the tail segments. For example,
ghci> segments "abc"

["","a","ab","abc","","b","bc","","c",""]

The empty sequence appears four times in this list, once for every tail segment.

Direct evaluation of
mss
will take a number of steps proportional to
n
³
on a list of length
n
. There are about
n
²
segments, and summing each of them will take
n
steps, so in total it will take
n
³
steps. It is not obvious that we can do better than cubic time for this problem.

However, let’s see where some program calculation leads us. We can start by installing the definition of
segments
:
maximum . map sum . concat . map inits . tails

Searching for a law we can apply, we spot that

map f . concat = concat . map (map f)

applies to the subterm
map sum . concat
. That gives
maximum . concat . map (map sum) . map inits . tails

Now we can use the law
map f . map g = map (f . g)
to give
maximum . concat . map (map sum . inits) . tails

Oh, we can also use the law

maximum . concat = maximum . map maximum

can’t we? No, not unless the argument to
concat
is a nonempty list of nonempty lists, because the maximum of the empty list is undefined. In the present example the rule is valid because both
inits
and
tails
return nonempty lists. That leads to
maximum . map (maximum . map sum . inits) . tails
The next step is to use the property of
scanl
described in the previous section, namely
map sum . inits = scanl (+) 0

That leads to

maximum . map (maximum . scanl (+) 0) . tails

Already we have reduced a
n
³
algorithm to a
n
²
one, so we are making progress. But now we appear stuck since there is no law in our armoury that seems to help.

The next step obviously concerns
maximum . scanl (+) 0
. So, let’s see what we can prove about
foldr1 max . scanl (+) 0

This looks like a fusion rule, but can
scanl (+) 0
be expressed as a
foldr
? Well, we do have, for instance,
scanl (+) 0 [x,y,z]

= [0,0+x,(0+x)+y,((0+x)+y)+z]

= [0,x,x+y,x+y+z]

= 0:map (x+) [0,y,y+z]

= 0:map (x+) (scanl (+) 0 [y,z])

This little calculation exploits the associativity of
(+)
and the fact that
0
is the identity element of
(+)
. The result suggests, more generally, that
scanl (@) e = foldr f [e]

where f x xs = e:map (x@) xs

provided that
(@)
is associative with identity
e
. Let us take this on trust and move on to the conditions under which
foldr1 (<>) . foldr f [e] = foldr h b

where f x xs = e:map (x@) xs

It is immediate that
foldr1 (<>)
is strict and
foldr1 (<>) [e] = e
, so we have
b = e
. It remains to check the third proviso of the fusion rule: we require
h
to satisfy
foldr1 (<>) (e:map (x@) xs) = h x (foldr1 (<>) xs)
for all
x
and
xs
. The left-hand side simplifies to

e <> (foldr1 (<>) (map (x@) xs))
Taking the singleton case
xs = [y]
, we find that

h x y = e <> (x @ y)

That gives us our definition of
h
, but we still have to check that
foldr1 (<>) (e:map (x@) xs) = e <> (x @ foldr1 (<>) xs)
Simplifying both sides, this equation holds provided

foldr1 (<>) . map (x@) = (x@) . foldr1 (<>)

This final equation holds provided
(@)
distributes
over
(<>)
; that is
x @ (y <> z) = (x @ y) <> (x @ z)

The proof is left as an exercise.

Does addition distribute over (binary) maximum? Yes:

x + (y `max` z) = (x + y) `max` (x + z)

x + (y `min` z) = (x + y) `min` (x + z)

Back to the maximum segment sum. We have arrived at

maximum . map (foldr (@) 0) . tails

where x @ y = 0 `max` (x + y)

What we have left looks very like an instance of the
scanl
rule of the previous section, except that we have a
foldr
not a
foldl
and a
tails
not an
inits
. But a similar calculation to the one about
scanl
reveals
map (foldr f e) . tails = scanr f e

where

scanr :: (a -> b -> b) -> b -> [a] -> [b]

scanr f e []
= [e]

scanr f e (x:xs) = f x (head ys):ys

where ys
= scanr f e xs

The function
scanr
is also defined in the standard prelude. In summary,
mss = maximum . scanr (@) 0

where x @ y = 0 `max` (x + y)

The result is a linear-time program for the maximum segment sum.

Exercise A

In
Chapter 3
we defined multiplication on natural numbers. The following definition is slightly different:
mult :: Nat -> Nat -> Nat

mult Zero y = Zero

mult (Succ x) = mult x y + y

Prove that
mult (x+y) z = mult x z + mult y z
. You can use only the facts that
x+0 = x
and that
(+)
is associative. That means a long think about which variable
x
,
y
or
z
is the best one on which to do the induction.

Exercise B

Prove that

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

for all finite lists
xs
and
ys
. You may assume that
(++)
is associative.

Exercise C

Recall our friends Eager Beaver and Lazy Susan from Exercise D in
Chapter 2
. Susan happily used the expression
head . map f
, while Beaver would probably prefer
f . head
. Wait a moment! Are these two expressions equal? Carry out an induction proof to check.

Exercise D

Recall the cartesian product function
cp :: [[a]] -> [[a]]
from the previous chapter. Give a definition of the form
cp = foldr f e
for suitable
f
and
e
. You can use a list comprehension for the definition of
f
if you like.

The rest of this exercise concerns the proof of the identity

length . cp = product . map length

where
product
returns the result of multiplying a list of numbers.

1. Using the fusion theorem, express
length.cp
as an instance of
foldr
.

2. Express
map length
as an instance of
foldr
.

3. Using the fusion theorem again, express
product . map length
as an instance of
foldr
.

4. Check that the two results are identical. If they aren’t, your definition of
cp
was wrong.

Exercise E

The first two arguments of
foldr
are replacements for the constructors
(:) :: a -> [a] -> [a]

[]
:: [a]

of lists. A fold function can be defined for any data type: just give replacements for the constructors of the data type. For example, consider
data Either a b = Left a | Right b

To define a fold for
Either
we have to give replacements for
Left :: a -> Either a b

Right :: b -> Either a b

That leads to

foldE :: (a -> c) -> (b -> c) -> Either a b -> c
foldE f g (Left x) = f x

foldE f g (Right x) = g x

The type
Either
is not a recursive data type and
foldE
is not a recursive function. In fact
foldE
is a standard prelude function, except that it is called
either
not
foldE
.

Now define fold functions for

data Nat = Zero | Succ Nat

data NEList a = One a | Cons a (NEList a)

The second declaration introduces nonempty lists.

What is wrong with the Haskell definition of
foldr1
?

Exercise F

Prove that

foldl f e xs = foldr (flip f) e (reverse xs)

for all finite lists
xs
. Also prove that

foldl (@) e xs = foldr (<>) e xs
for all finite lists
xs
, provided that

(x <> y) @ z = x <> (y @ z)

e @ x = x <> e

Exercise G

Using

foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys

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

prove that

foldl f e . concat = foldl (foldl f) e

foldr f e . concat = foldr (flip (foldr f)) e

Exercise H

Mathematically speaking, what is the value of

sum (scanl (/) 1 [1..]) ?

Exercise I

Calculate the efficient definition of
scanr
from the specification
scan r f e = map (foldr f e) . tails

Exercise J

Consider the problem of computing

mss :: [Int] -> Int

mss = maximum . map sum . subseqs

where
subseqs
returns all the subsequences of a finite list, including the list itself:
subseqs :: [a] -> [[a]]

subseqs []
= [[]]

subseqs (x:xs) = xss ++ map (x:) xss

where xss = subseqs xs

Find a more efficient alternative for
mss
.

Exercise K

This question is in pieces.

1. The function
takePrefix p
applied to a list
xs
returns the longest initial segment of
xs
that satisfies
p
. Hence
takePrefix :: ([a] -> Bool) -> [a] -> [a]

What are the values of the following expressions?

takePrefix nondec [1,3,7,6,8,9]

takePrefix (all even) [2,4,7,8]

Complete the right-hand side of

takePrefix (all p) = ...

Give a definition of
takePrefix
in terms of standard functions, including
inits
. We will return to
takePrefix
in the final part of this question.

2. The functions
one
and
none
are defined by the equations
one x
= [x]

none x = []

Complete the right-hand side of the following identities:

none . f
= ...

map f . none = ...

map f . one
= ...

3. Recall that
fork (f,g) x = (f x,g x)
. Complete the identities
fst . fork (f,g) = ...

snd . fork (f,g) = ...

fork (f,g) . h
= ...

4. Define

test p (f,g) x = if p x then f x else g x

Complete the right-hand sides of

test p (f,g) . h = ...

h . test p (f,g) = ...

The function
filter
can be defined by

filter p = concat . map (test p (one,none))

Using the identities above, together with other standard identities, prove using equational reasoning that

filter p = map fst . filter snd . map (fork (id,p))

(
Hint
: as always in calculations, start with the more complicated side.)

5. Recall the standard prelude functions
curry
and
uncurry
from the answer to Exercise K in
Chapter 4
:
curry :: ((a,b) -> c) -> a -> b -> c

curry f x y = f (x,y)

uncurry :: (a -> b -> c) -> (a,b) -> c

uncurry f (x,y) = f x y

Complete the right-hand side of

map (fork (f,g)) = uncurry zip . (??)

6. Returning to
takePrefix
, use equational reasoning to calculate an efficient program for the expression
takePrefix (p . foldl f e)

that requires only a linear number of applications of
f
.

Answer to Exercise A

The proof is by induction on
y
:

Case
0

mult (x+0) z
mult x z + mult 0 z
=
{since
x + 0=x
}
=
{
mult.1
}