Thinking Functionally with Haskell (53 page)

Exercise J

How many segments of a list of length
n
are there? The definition of
rewritesSeg
is inefficient because the empty segment appears
n
+1 times as the middle component of the segments of a list of length
n
. That means matching with
id
is performed
n
+1 times instead of just once. How would you rewrite
segments
to eliminate these duplicates?

Exercise K

Prove that
cmap f . cmap g = cmap (cmap f . g)
. The laws needed are:
defn cmap:
cmap f = concat . map f

map functor:
map f . map g = map (f.g)

map after concat:
map f . concat = concat . map (map f)
concat twice:
concat . concat = concat . map concat
Exercise L

The
cmap-cpp
law is as follows:

cmap (cpp . (one
f)) . cpp = cpp . (id
cmap f)

Prove it from the laws

cmap after cmap:
cmap f . map g = cmap (f . g)
cmap after cpp:
cmap cpp . cpp = cpp . (concat * concat)
cross bifunctor:
(f * g) . (h
k) = (f . h)
(g . k)
map after cpp:
map (f
g) . cpp = cpp . (map f
map g)
defn cmap:
cmap f = concat . map f

concat after id:
concat . map one = id

Can a calculator conduct the proof?

Answer to Exercise A

We would want expressions as labels of nodes and law names as labels of edges. That gives
type Calculation = Tree Expr LawName

data Tree a b = Node a [(b,Tree a b)]

Answer to Exercise B

They would both cause the calculator to spin off into an infinite calculation. For example,
map foo

=
{map functor}

map foo . map id

=
{map functor}

map foo . map id . map id

and so on.

Answer to Exercise C

The expression
map f . map g h
is perfectly valid by the rules of syntax, but of course it shouldn’t be. The evaluator does not force the restriction that each appearance of one and the same constant should possess the same number of arguments. The reason the functor law can be matched successfully against the expression is that in the definition of
matchA
the function
zip
truncates the two arguments to the second
map
to one. A better calculator should check that each constant has a fixed arity.

Answer to Exercise D

The cryptic message is ‘head of empty list’. The first parse fails because the law is missing its name, and the second is missing an equals sign. Use of the strange law would cause the calculator to fall over because pattern-matching with the left-hand side would not bind
h
to any expression, causing an error when the binding for
h
is requested. The calculator should have checked that every variable on the right-hand side of a law appears somewhere on the left-hand side.

Answer to Exercise E

The code for
showsPrec
takes the form

showsPrec p (Con f [e1,e2])

| isOp f = expression1 e1 e2

showsPrec p (Con f es)

= expression2 es

A more ‘mathematical’ style would have been to write

showsPrec p (Con f [e1,e2])

| isOp f = expression1 e1 e2

| otherwise = expression2 [e1,e2]

showsPrec p (Con f es) = expression2 es

The point is this: in a given clause if a pattern does not match the argument, or if it does but the guard fails to be true, the clause is abandoned and the next clause is chosen.

Answer to Exercise F

There are two rewrites, not one:

bar (a . b . c) . baz id . c

bar (a . b) . baz c

The calculator would pick the first subexpression that matches, and that means the first rewrite is chosen. Perhaps it would be better to arrange that
rewritesSeg
is applied to longer segments before shorter ones.

Answer to Exercise G

No, not with our definition of
match
. They can be matched by binding
f
to the expression
bar (daz a) b
provided
g
is bound to
daz a
and
h
to
b
, but our definition of
match
does not perform full unification.

Answer to Exercise H

To take just one example out of many, consider the law

if p f g . h = if (p . h) (f . h) (g . h)

The left-hand side matches
if a b c
with
h
bound to
id
, and the result is again the same expression.

Answer to Exercise I

The temptation is to define

everyOne f = cp . map f

but that doesn’t work if
f
returns no alternatives for some element. Instead we have to define
everyOne :: (a -> [a]) -> [a] -> [[a]]

everyOne f = cp . map (possibly f)

possibly f x = if null xs then [x] else xs

where xs = f x

In this version,
f
returns a nonempty list of alternatives.

Answer to Exercise J

There are (
n
+1)(
n
+2)/2 segments of a list of length
n
. The improved definition is
segments xs = [([],[],xs] ++

[(as,bs,cs)

| (as,ys) <- splits xs,

(bs,cs) <- tail (splits ys)]

Answer to Exercise K

The calculator produced:

cmap f . cmap g

=
{defn cmap}

concat . map f . cmap g

=
{defn cmap}

concat . map f . concat . map g

=
{map after concat}

concat . concat . map (map f) . map g

=
{map functor}

concat . concat . map (map f . g)

=
{concat after concat}

concat . map concat . map (map f . g)

=
{map functor}

concat . map (concat . map f . g)

=
{defn cmap}

concat . map (cmap f . g)

=
{defn cmap}

cmap (cmap f . g)

Answer to Exercise L

The human proof is:

cmap (cpp . (one * g)) . cpp

=
{cmap after cmap (backwards)}

cmap cpp . map (one * g) . cpp

=
{map after cpp}

cmap cpp . cpp . (map one * map g)

=
{cmap after cpp}

cpp . (concat * concat) . (map one * map g)

=
{cross bifunctor}

cpp . ((concat . map one) * concat (map g))

=
{defn cmap (backwards)}

cpp . ((concat . map one) * cmap g)

=
{concat after id}

cpp . (id * cmap g)

No, the calculation cannot be performed automatically. The
cmap after cmap
law cannot be installed in the backwards direction without causing the calculator to loop (see Exercise B).

The calculator in this chapter is based on an undocumented theorem prover by Mike Spivey, a colleague at Oxford. Ross Paterson of City University, London, has produced a version with built-in functor laws that can be applied in both directions when necessary.

One state-of-the-art proof assistant is Coq; see
http://coq.inria.fr/
.

Θ asymptotic notation,
157

⌊−⌋ floor function,
46
,
52
,
62

⊥ undefined value,
24
,
28
,
30
,
104
,
177
,
215
,
217
,
226
,
233

π
,
50
,
215

⊑ approximation ordering,
217

(%)
integral ratio,
50

""
empty list of characters,
18

"
double quotes,
4

'
single quote,
3

(!!)
list-indexing operation,
9

(!)
array-indexing operation,
261

($!)
strict application operator,
153
,
252

($)
application operator,
153

(&&)
boolean conjunction,
10

()
null tuple,
30
,
33
,
240

(**)
exponentiation,
59

(,)
pair constructor,
74
,
146

(-)
subtraction operator,
27

(->)
function type,
1

(.)
function composition,
3
,
15
,
31

(//)
array update operation,
262

(/=)
inequality test,
9

(:)
cons, list constructor,
64

(<=)
comparison test,
9
,
76

(<=<)
right-to-left Kleisli composition,
247

(==)
equality test,
9

(>=>)
left-to-right Kleisli composition,
247

(>>)
sequence operation,
240

(>>=)
monadic bind,
241
,
279

(^)
exponentiation,
59

(^^)
exponentiation,
59

(||)
boolean disjunction,
32

.hs
Haskell script,
35
,
227

.lhs
literate Haskell script,
8
,
35
,
227

:load
instruction,
13

:set
instruction,
13
,
148

:type
instruction,
22

@
as patterns,
see
patterns

[]
empty list,
17
,
63
,
64
,
104
,
121
,
151

\
escape character,
18

\n
newline character,
3
,
18

\t
tab character,
18

`
back-quote,
9
,
25

(++)
list concatenation,
10
,
15
,
69
,
113

n+k
patterns,
111

abs
,
50
,
54

absolute value,
see
abs

abstract data types,
194
,
239
,
259

abstract syntax trees,
201

accumArray
,
260

accumulating functions,
260

accumulating parameters,
159
,
171
,
288
,
289
,
323

actions,
239

Agda,
48

Algorithm Design,
145
,
154

all
,
94

alphabetical order,
5
,
19

anagrams
,
16

and
,
74

anti-symmetric relation,
217

any
,
102

approx
,
218

Array
,
259

array
,
259

arrays

immutable,
259

mutable,
254

associative operations,
15
,
26
,
70
,
112
,
113
,
119
,
124
,
129
,
184
,
231
,
246
,
247
,
281
,
326

assocs
,
262

asymptotic complexity,
155

Augustsson, L.,
47

auxiliary results,
114
,
117
,
140

base cases,
see
induction

Bentley, J.,
21
,
127
,
144

Bifunctor
,
82

bifunctors,
82
,
87
,
302
,
326

binary operators,
25

binary search,
54

binary trees,
165
,
249

binding power,
2
,
14
,
25

Bird, R.,
87
,
180

blank characters,
3

BNF (Backus-Naur form),
286
,
305