Thinking Functionally with Haskell (22 page)

mult x z
mult x z + 0

=
{since
x + 0 = x
}

mult x z

Case
y+1

mult (x+(y+1)) z
mult x z + mult (y+1) z
=
{as
(+)
is associative}
=
{
mult.2
}

mult ((x+y)+1) z
mult x z + (mult y z + z)
=
{
mult.2
}
=
{since
(+)
is associative}

mult (x+y) z + z
(mult x z + mult y z) + z
=
{induction}

(mult x z + mult y z) + z

Answer to Exercise B

The proof is by induction on
xs
:

Case
[]

reverse ([]++ys)
reverse ys ++ reverse []

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

reverse ys
reverse ys ++ []

=
{since
xs ++ [] = xs
}

reverse ys

Case
x:xs

reverse ((x:xs)++ys)

=
{
++.2
}

reverse (x:(xs++ys))

=
{
reverse.2
}

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

=
{induction}

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

and

reverse ys ++ reverse (x:xs)

=
{
reverse.2
}

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

=
{since
(++)
is associative}

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

Answer to Exercise C

We have to prove that

head (map f xs) = f (head xs)

for all lists
xs
, finite, partial or infinite. The case
undefined
and the inductive case
x:xs
are okay, but the case
[]
gives
head (map f []) = head [] = undefined

f (head [])
= f undefined

Hence the law holds only if
f
is a strict function. Eager Beaver is not bothered by this since he can only construct strict functions.

Answer to Exercise D

We have

cp = foldr op [[]]

where op xs xss = [x:ys | x <- xs, ys <- xss]

1.
length . cp = foldr h b
provided
length
is strict (it is) and
length [[]] = b

length (op xs xss) = h xs (length xss)

The first equation gives
b = 1
and as

length (op xs xss) = length xs * length xss

the second equation gives
h = (*) . length
.

2.
map length = foldr f []
, where
f xs ns = length xs:ns
. A shorter definition is
f = (:) . length
.

3.
product . map length = foldr h b
provided
product
is strict (it is) and
product [] = b

product (length xs:ns) = h xs (product ns)

The first equation gives
b = 1
, and as

product (length xs:ns) = length xs * product ns

the second equation gives
h = (*) . length
.

4. The two definitions of
h
and
b
are identical.

Answer to Exercise E

The definition of
foldN
is straightforward:

foldN :: (a -> a) -> a -> Nat -> a

foldN f e Zero = e

foldN f e (Succ n) = f (foldN f e n)

In particular,

m+n = foldN Succ m n

m*n = foldN (+m) Zero n

m^n = foldN (*m) (Succ Zero) n

For nonempty lists, the definition of
foldNE
is:

foldNE :: (a -> b -> b) -> (a -> b) -> NEList a -> b
foldNE f g (One x) = g x

foldNE f g (Cons x xs) = f x (foldNE f g xs)

To be a proper fold over nonempty lists, the correct definition of
foldr1
should have been
foldr1 :: (a -> b -> b) -> (a -> b) -> [a] -> b
foldr1 f g [x] = g x

foldr1 f g (x:xs) = f x (foldr1 f g xs)

The Haskell definition of
foldr1
restricts
g
to be the identity function.

Answer to Exercise F

Write
g = flip f
for brevity. We prove that

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

for all finite lists
xs
by induction:

Case
[]

foldl f e []
foldl g e (reverse [])
=
{
foldl.1
}
=
{
reverse.1
}

e
foldl g e []

=
{
foldl.1
}

e

Case
x:xs

foldl f e (x:xs)

=
{
foldl.2
}

foldl f (f e x) xs

=
{induction}

foldr g (f e x) (reverse xs)

and

foldr g e (reverse (x:xs))

=
{
reverse.2
}

foldr g e (reverse xs ++ [x])

=
{claim: see below}

foldr g (foldr g e [x]) (reverse xs)

=
{since
foldr (flip f) e [x] = f e x
}

foldr g (f e x) (reverse xs)

The claim is that

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

We leave the proof to the reader. By the way, we have the companion result that
foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys

Again, the proof is left to you.

We prove

foldl (@) e xs = foldr (<>) e xs

for all finite lists
xs
by induction. The base case is trivial. For the inductive case:
Case
x:xs

foldl (@) e (x:xs)
foldr (<>) e (x:xs)
=
{
foldl.2
}
=
{
foldr.2
}

foldl (@) (e @ x) xs
x <> foldr (<>) e xs
=
{given that
e @ x = x <> e
}
=
{induction}

foldl (@) (x <> e) xs
x <> foldl (@) e xs
The two sides have simplified to different results. We need another induction hypothesis:
foldl (@) (x <> y) xs = x <> foldl (@) y xs

The base case is trivial. For the inductive case

Case
z:zs

foldl (@) (x <> y) (z:zs)

=
{
foldl.2
}

foldl (@) ((x <> y) @ z) zs

=
{since
(x <> y) @ z = x <> (y @ z)
}

foldl (@) (x <> (y @ z)) zs

=
{induction}

x <> foldl (@) (y @ z) zs

and

x <> foldl (@) y (z:zs)

=
{
foldl.2
}

x <> foldl (@) (y @ z) zs

Answer to Exercise G

The proofs are by induction. The base cases are easy and the inductive cases are
foldl f e (concat (xs:xss))

=
{definition of
concat
}

foldl f e (xs ++ concat xss)

=
{given property of
foldl
}

foldl f (foldl f e xs) (concat xss)

=
{induction}

foldl (foldl f) (foldl f e xs) xss

=
{definition of
foldl
}

foldl (foldl f) e (xs:xss)

and

foldr f e (concat (xs:xss))

=
{definition of
concat
}

foldr f e (xs ++ concat xss)

=
{given property of
foldr
}

foldr f (foldr f e (concat xss)) xs

=
{using
flip
}

flip (foldr f) xs (foldr f e (concat xss))

=
{induction}

flip (foldr f) xs (foldr (flip (foldr f)) e xss)

=
{definition of
foldr
}

foldr (flip (foldr f)) e (xs:xss)

Answer to Exercise H

Mathematically speaking,

sum (scanl (/) 1 [1..]) = e

since
Computationally speaking, replacing
[1..]
by a finite list
[1..n]
gives an approximation to
e
. For example,
ghci> sum (scanl (/) 1 [1..20])

2.7182818284590455

ghci> exp 1

2.718281828459045

The standard prelude function
exp
takes a number
x
and returns
e
^x
. By the way, the prelude function
log
takes a number
x
and returns log
_e
x
. If you want logarithms in another base, use
logBase
whose type is
logBase :: Floating a => a -> a -> a

Answer to Exercise I

We synthesise a more efficient definition by cases. The base case yields

scanr f e [] = [e]

and the inductive case
x:xs
is:
scanr f e (x:xs)

=
{specification}

map (foldr f e) (tails (x:xs))

=
{
tails.2
}

map (foldr f e) ((x:xs):tails xs)

=
{definition of
map
}

foldr f e (x:xs):map (foldr f e) (tails xs)

=
{
foldr.2
and specification}

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

=
{claim:
foldr f e xs = head (scanr f e xs)
}

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

Answer to Exercise J

Firstly,

subseqs = foldr op [[]]

where op x xss = xss ++ map (x:) xss

Appeal to the fusion law yields

map sum . subseqs = foldr op [0]

where op x xs = xs ++ map (x+) xs

A second appeal to fusion yields

maximum . map sum . subseqs = foldr op 0

where op x y = y `max` (x+y)

That will do nicely. Of course,
sum . filter (>0)
also does the job.

Answer to Exercise K

1. We have

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

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

The identity is

takePrefix (all p) = takeWhile p

The specification is

takePrefix p = last . filter p . inits

2. We have

none . f = none

map f . none = none

map f . one = one . f

3. We have

fst . fork (f,g) = f

snd . fork (f,g) = g

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

4. We have

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

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

The reasoning is:

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

=
{definition of
filter
}

map fst . concat . map (test snd (one,none)) .

map (fork (id,p))

=
{since
map f . concat = concat . map (map f)
}

concat . map (map fst . test snd (one,none) .

fork (id,p))

=
{second law of
test
; laws of
one
and
none
}

concat . map (test snd (one . fst,none) .

fork (id,p))

=
{first law of
test
; laws of
fork
}

concat . map (test p (one . id, none . fork (id,p)))

=
{laws of
id
and
none
}