Thinking Functionally with Haskell (53 page)
Read Thinking Functionally with Haskell Online
Authors: Richard Bird
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
⊥ undefined value,
24
,
28
,
30
,
104
,
177
,
215
,
217
,
226
,
233
⊑ 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
(**)
exponentiation,
59
(-)
subtraction operator,
27
(->)
function type,
1
(.)
function composition,
3
,
15
,
31
(//)
array update operation,
262
(/=)
inequality test,
9
(:)
cons, list constructor,
64
(<=<)
right-to-left Kleisli composition,
247
(==)
equality test,
9
(>=>)
left-to-right Kleisli composition,
247
(>>)
sequence operation,
240
(^)
exponentiation,
59
(^^)
exponentiation,
59
(||)
boolean disjunction,
32
.lhs
literate Haskell script,
8
,
35
,
227
:load
instruction,
13
:type
instruction,
22
@
as patterns,
see
patterns
[]
empty list,
17
,
63
,
64
,
104
,
121
,
151
\
escape character,
18
\t
tab character,
18
(++)
list concatenation,
10
,
15
,
69
,
113
n+k
patterns,
111
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
all
,
94
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
base cases,
see
induction
Bifunctor
,
82
binary operators,
25
binary search,
54
blank characters,
3