Thinking Functionally with Haskell (52 page)

=
{defn xmatchesA}

cmap xmatchesA . cpp . (one * alignments)

Ah, it doesn’t go through. Inspecting the gap in the calculation, it seems we need both the bifunctor law of
*
and a claim relating
cmap
and
cup
:
cross bifunctor: (f * g) . (h
k) = (f . h)
(g . k)

cmap-cup: cmap (cup . (one * g)) . cpp = cup . (id * cmap g)

The calculator is then happy:

xmatch

=
{defn xmatch}

cup . (one * match)

=
{defn match}

cup . (one * (cmap matchesA . alignments))

=
{cross bifunctor}

cup . (id * cmap matchesA) . (one * alignments)

=
{cmap-cup}

cmap (cup . (one
matchesA)) . cpp . (one
alignments)

=
{defn xmatchesA}

cmap xmatchesA . cpp . (one * alignments)

That still leaves us with the claim; apart from the fact that it works we have no reason to suppose it is true. However, we can get the calculator to prove it by using another law that is not specific to matching. We leave the proof as Exercise M. Define the additional laws
defn cup: cup = cmap unify . cpp

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

The calculator then produces

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

=
{defn cup}

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

=
{cmap after cmap}

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

=
{cmap-cpp}

cmap unify . cpp . (id * cmap g)

=
{defn cup}

cup . (id * cmap g)

Good. It seems that the
cmap-cup
law is valid, and it even might be useful again later on. Now let us return to the main point, which is to express
xmatchesA
recursively by two equations of the form
xmatchesA . (id * nil) = ...

xmatchesA . (id * cons) = ...

The hope is that such a definition will not involve
unify
. It is not at all clear what laws we need for this purpose. Instead, we will write down every law we can think of that might prove useful. The first group consists of our main definitions:
defn match:
match = cmap matchesA . alignments
defn matchesA:
matchesA = combine . map matchA
defn xmatch:
xmatch = cup . (one * match)
defn xmatchesA:
xmatchesA = cup . (one * matchesA)
defn xmatchA:
xmatchA = cup . (one * matchA)
defn combine:
combine = cmap unifyAll . cp
The second group are some new laws about
cmap
:

cmap after map:
cmap f . map g = cmap (f . g)
cmap after concat:
cmap f . concat = cmap (cmap f)
cmap after nil:
cmap f . nil = nil

cmap after one:
cmap f . one = f

The third group are some new laws about
map
:

map after nil: map f . nil = nil

map after one: map f . one = one . f

map after cons: map f . cons = cons . (f * map f)

map after concat: map f . concat = concat . map (map f)

The fourth group concerns
cup
:

cup assoc: cup . (id * cup) = cup . (cup * id) . assocl

cup ident: cup . (f * (one . nil)) = f . fst

cup ident: cup . ((one . nil) * g) = g . snd

assocl: assocl. (f
(g
h)) = ((f
g)
h) . assocl

Finally we add in various other definitions and laws:

cross bifunctor: (f * g) . (h
k) = (f . h)
(g . k)

cross bifunctor: (id * id) = id

defn cp: cp . nil = one . nil

defn cp: cp . cons = map cons . cpp . (id * cp)

defn unifyAll: unifyAll . nil = one . nil

defn unifyAll: unifyAll . cons = cup . (one * unifyAll)

unify after nil: unify . (id * nil) = one . fst

That’s a total of 30 laws (including the two
map
functor laws and three laws about
cmap
that we haven’t repeated). We cross our fingers and hope:
xmatchesA . (id * nil)

=
{defn xmatchesA}

cup . (one * matchesA) . (id * nil)

=
{cross bifunctor}

cup . (one * (matchesA . nil))

=
{defn matchesA}

cup . (one * (combine . map matchA . nil))

=
{map after nil}

cup . (one * (combine . nil))

=
{defn combine}

cup . (one * (cmap unifyAll . cp . nil))

=
{defn cp}

cup . (one * (cmap unifyAll . one . nil))

=
{cmap after one}

cup . (one * (unifyAll . nil))

=
{defn unifyAll}

cup . (one * (one . nil))

=
{cup ident}

one . fst

That’s gratifying. We have shown that
xmatchesA sub [] = [sub]
. However, the recursive case cannot be established so easily. Instead we have to guess the result and then try to prove it. Here is the desired result, first expressed in pointed form and then in pointless form:
xmatchesA sub (ae:aes)

= concat [xmatchesA sub' aes | sub' <- xmatchA sub ae]

xmatchesA . (id * cons)

= cmap xmatchesA . cpp . (xmatchA * one) . assocl

We can perform simplification with the right-hand side (we temporarily remove the definitions of
xmatchA
and
matchesA
from
laws2
):
cmap xmatchesA . cpp . (xmatchA * one) . assocl

=
{defn xmatchesA}

cmap (cup . (one * matchesA)) . cpp . (xmatchA * one) . assocl

=
{cmap-cup}

cup . (id * cmap matchesA) . (xmatchA * one) . assocl

=
{cross bifunctor}

cup . (xmatchA * (cmap matchesA . one)) . assocl

=
{cmap after one}

cup . (xmatchA * matchesA) . assocl

Now we would like to show

xmatchesA . (id * cons)

= cup . (xmatchA * matchesA) . assocl

But unfortunately the calculator can’t quite make it. The gap appears here:

cup . ((cup . (one * matchA)) * matchesA)

=
{... ??? ...}

cup . (one
(cup . (matchA
matchesA))) . assocl

The gap is easily eliminable by hand:

cup . ((cup . (one * matchA)) * matchesA)

=
{cross bifunctor (backwards)}

cup . (cup * id) . ((one
matchA)
matchesA)

=
{cup assoc}

cup . (id * cup) . assocl . ((one
matchA)
matchesA)

=
{assocl}

cup . (id * cup) . (one
(matchA
matchesA)) . assocl

=
{cross bifunctor}

cup . (one
(cup . (matchA
matchesA))) . assocl

Once again, the inability to apply laws in both directions is the culprit. Instead of trying to force the laws into a form that would be acceptable to the calculator, we leave it here with the comment ‘A hand-finished product!’.

To round off the example, here is the program we have calculated:

match = xmatch emptySub

xmatch sub (e1,e2)

= concat [xmatchesA sub aes | aes <- alignments (e1,e2)]

xmatchesA sub [] = [sub]

xmatchesA sub (ae:aes)

= concat [xmatchesA sub' aes | sub' <- xmatchA sub ae]

xmatchA sub (Var v,e) = extend sub v e

xmatchA sub (Con k1 es1,Compose [Con k2 es2])

| k1==k2 = xmatches sub (zip es1 es2)

xmatchA _ = []

The missing definition is that of
xmatches
. But exactly the same treatment for
xmatchesA
goes through for
matches
, and we end up with
xmatches sub [] = [sub]

xmatches sub ((e1,e2):es)

= concat [xmatches sub' es | sub' <- xmatch sub (e1,e2)]

The positive conclusion of these two exercises is that one can indeed get the calculator to assist in the construction of formal proofs. But there remains the need for substantial human input to the process, to set up appropriate laws, to identify subsidiary claims and to control the order in which calculations are carried out. The major negative conclusion is that it is a significant failing of the calculator to be unable to apply laws in both directions. The functor laws are the major culprits, but there are others as well (see the exercises for some examples). The calculator can be improved in a number of ways, but we leave further discussion to the exercises.

There are three other aspects worth mentioning about the calculator. Firstly, the complete calculator is only about 450 lines of Haskell, and the improved version is even shorter. That alone is a testament to the expressive power of functional programming. Secondly, it does seem a viable approach to express laws as purely functional equations and to use a simple equational logic for conducting proofs. To be sure, some work has to be done to express definitions in point-free form, but once this is achieved, equational logic can be surprisingly effective.

The third aspect is that, apart from parsing, no monadic code appears in the calculator. In fact, earlier versions of the calculator did use monads, but gradually they were weeded out. One reason was that we found the code became simpler without monads, without significant loss of efficiency; another was that we wanted to set things up for the extended exercise in improving the calculator. Monads are
absolutely necessary for many applications involving interacting with the world, but they can be overused in places where a purely functional approach would be smoother.

On that note, we end.

Exercise A

Suppose we did want
calculate
to return a tree of possible calculations. What would be a suitable tree to use?

Exercise B

Why should the laws

map (f . g) = map f . map g

cmap (f . g) = cmap f . map g

never
be used in calculations, at least if they are given in the form above?

Exercise C

Here is a calculation, as recorded by the calculator

map f . map g h

=
{map functor}

map (f . g)

Explain this strange and clearly nonsensical result. What simple change to the calculator would prevent the calculation from being valid?

Exercise D

On the same general theme as the previous question, one serious criticism of the calculator is that error messages are totally opaque. For example, both
parse law "map f . map g = map (f . g)"

parse law "map functor: map f . map g map (f . g)"

cause the same cryptic error message. What is it? What would be the effect of using the law
strange: map f . map g = map h

in a calculation?

Again, what change to the calculator would prevent such a law from being acceptable?

Exercise E

The definition of
showsPrec
for atoms makes use of a fact about Haskell that we haven’t needed before. And the same device is used in later calculator functions that mix a pattern-matching style with guarded equations. What is the fact?

Exercise F

Define

e1 = foo (f . g) . g

e2 = bar f . baz g

List the expressions that
rewrites (e1,e2)
produces when applied to the expression
foo (a . b . c) . c
. Which one would the calculator pick?

Exercise G

Can the calculator successfully match
foo f . foo f
with the expression
foo (bar g h) . foo (bar (daz a) b) ?

Exercise H

It was claimed in the text that it is possible to apply a perfectly valid non-trivial law that will leave some expressions unchanged. Give an example of such a law and an expression that is rewritten to itself.

Exercise I

The function
anyOne
used in the definition of
rewrites
installs a single choice, but why not use
everyOne
that installs every choice at the same time? Thus if
f 1 = [-1,-2]
and
f 2 = [-3,-4]
, then
everyOne f [1,2] = [[-1,-3],[-1,-4],[-2,-3],[-3,-4]]

Using
everyOne
instead of
anyOne
would mean that a rewrite would be applied to every possible subexpression that matches a law. Give a definition of
everyOne
.