Thinking Functionally with Haskell (51 page)

| v1==v2 = if e1==e2 then compatible sub1' sub2'

else False

| v1>v2 = compatible sub1 sub2'

The union operation is defined in a similar style:

union [] sub2 = sub2

union sub1 [] = sub1

union sub1@((v1,e1):sub1') sub2@((v2,e2):sub2')

| v1= (v1,e1):union sub1' sub2

| v1==v2 = (v1,e1):union sub1' sub2'

| v1>v2
= (v2,e2):union sub1 sub2'

The function
unifyAll
returns either an empty list or a singleton list:
unifyAll :: [Subst] -> [Subst]

unifyAll = foldr f [emptySub]

where f sub subs = concatMap (unify sub) subs

That completes the definitions we need. Here is the module declaration:

module Substitutions

(Subst, unitSub, combine, apply)

where

import Expressions

import Utilities (cp)

import Data.Maybe (fromJust)

That makes nine modules in total for our calculator.

How useful is the calculator in practice? The only way to answer this question is to try it out on some examples. We are going to record just two. The first is the calculation we performed in
Chapter 5
about pruning the matrix of choices in Sudoku. In effect we want to prove
filter (all nodups . boxs) . expand . pruneBy boxs

= filter (all nodups . boxs) . expand

from the laws

defn pruneBy: pruneBy f = f . map pruneRow . f

expand after boxs: expand . boxs = map boxs . expand

filter with boxs: filter (p . boxs)

= map boxs . filter p . map boxs

boxs involution: boxs . boxs = id

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

map functor: map id = id

defn expand: expand = cp . map cp

filter after cp: filter (all p) . cp = cp . map (filter p)

law of pruneRow: filter nodups . cp . pruneRow

= filter nodups . cp

Here is the calculation exactly as performed by the calculator, except that we have broken some expressions across two lines, a task that should be left to a prettyprinter. Don’t bother to study it in detail, just note the important bit towards the end:
filter (all nodups . boxs) . expand . pruneBy boxs

=
{filter with boxs}

map boxs . filter (all nodups) . map boxs . expand .

pruneBy boxs

=
{defn pruneBy}

map boxs . filter (all nodups) . map boxs . expand .

boxs . map pruneRow . boxs

=
{expand after boxs}

map boxs . filter (all nodups) . map boxs . map boxs .

expand . map pruneRow . boxs

=
{map functor}

map boxs . filter (all nodups) . map (boxs . boxs) . expand .

map pruneRow . boxs

=
{boxs involution}

map boxs . filter (all nodups) . map id . expand .

map pruneRow . boxs

=
{map functor}

map boxs . filter (all nodups) . expand . map pruneRow . boxs

=
{defn expand}

map boxs . filter (all nodups) . cp . map cp . map pruneRow . boxs
=
{map functor}

map boxs . filter (all nodups) . cp . map (cp . pruneRow) . boxs

=
{filter after cp}

map boxs . cp . map (filter nodups) . map (cp . pruneRow) . boxs

=
{map functor}

map boxs . cp . map (filter nodups . cp . pruneRow) . boxs

=
{law of pruneRow}

map boxs . cp . map (filter nodups . cp) . boxs

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

map boxs . filter (all nodups) . map boxs . cp . map cp

=
{defn expand}

map boxs . filter (all nodups) . map boxs . expand

=
{filter with boxs}

filter (all nodups . boxs) . expand

Yes, the calculation fails. The reason is not hard to spot: we need to apply the law

expand after boxs: expand . boxs = map boxs . expand

in both directions, and the calculator simply cannot do that.

The solution is a hack. We add in the extra law

hack: map boxs . cp . map cp = cp . map cp . boxs

which is just the
expand
after
boxs
law written in the opposite direction and with
expand
replaced by its definition. Then the calculator is happy, producing the conclusion
....

map boxs . cp . map (filter nodups . cp) . boxs

=
{map functor}

map boxs . cp . map (filter nodups) . map cp . boxs

=
{filter after cp}

map boxs . filter (all nodups) . cp . map cp . boxs

=
{hack}

map boxs . filter (all nodups) . map boxs . cp . map cp

=
{defn expand}

map boxs . filter (all nodups) . map boxs . expand

=
{filter with boxs}

filter (all nodups . boxs) . expand

In both cases the calculations were performed in a fraction of a second, so efficiency does not seem to be an issue. And, apart from the hack, the calculations pass muster, being almost exactly what a good human calculator would produce.

Improving the calculator

Our second example is more ambitious: we are going to use the calculator to derive another version of the calculator. Look again at the definition of
match
. This relies on
combine
, which in turn involves a messy appeal to the unification of two substitutions, with all the paraphernalia of having to test them for compatibility and computing the union. A better idea is to compute the union of two substitutions only when one of them is a unit substitution. Then everything becomes simpler and probably faster. And the technique which describes this optimisation? Yes, it’s another example of accumulating parameters. Just as an accumulating parameter can avoid expensive uses of
++
operations, our hope is to avoid expensive
unify
operations.

First of all, here is the definition of
match
again, written with a couple of new subsidiary functions:
match = concatMap matchesA . alignments

matchesA = combine . map matchA

matchA (Var v,e) = [unitSub v e]

matchA (Con k1 es1,Compose [Con k2 es2])

| k1==k2 = matches (zip es1 es2)

matchA _ = []

matches = combine . map match

Note the cycle of dependencies of these functions:

match --> matchesA --> matchA --> matches --> match

These four functions are generalised as follows:

xmatch sub
= concatMap (unify sub) . match
xmatchA sub
= concatMap (unify sub) . matchA
xmatches sub
= concatMap (unify sub) . matches
xmatchesA sub = concatMap (unify sub) . matchesA

The additional argument in each case is an accumulating parameter. Our aim will
be to obtain new versions of these definitions, whose cycle of dependencies is the same as the one above: For the first calculation, we want to rewrite
match
in terms of
xmatch
, thereby linking the two groups of definitions. To save a lot of ink, we henceforth abbreviate
concatMap
to
cmap
. The three laws we need are
defn xmatch:
xmatch s = cmap (unify s) . match
unify of empty:
unify emptySub = one

cmap of one:
cmap one = id

In the first law we have to write
s
rather than
sub
(why?); the second two laws are the pointless versions of the facts that
unify emptySub sub = [sub]

cmap one xs = concat [[x] | x <- xs] = xs

The calculator is hardly stretched to give:

xmatch emptySub

=
{defn xmatch}

cmap (unify emptySub) . match

=
{unify of empty}

cmap one . match

=
{cmap of one}

match

Let us next deal with
xmatchA
. Because of the awkward pattern-matching style of definition of
matchA
, we simply record the following result of an easy (human) calculation:
xmatchA sub (Var v,e) = concat [unify sub (unitSub v e)]

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

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

xmatchA _ = []

If we introduce

extend sub v e = concat [unify sub (unitSub v e)]

then it is easy to derive

extend sub v e

= case lookup v sub of

Nothing -> [(v,e):sub]

Just e' -> if e==e' then [sub]

else []

No elaborate compatibility test, and no general union of two substitutions. Instead, as we promised earlier, we unify substitutions only with unit substitutions.

Having disposed of
xmatchA
we concentrate on the other three members of the quartet. Just as
xmatchA
is defined in terms of
xmatches
, so
xmatch
can be defined in terms of
xmatchesA
. Specifically, we want to prove that
xmatch s = cmap (xmatchesA s) . alignments

Here are the laws we need:

defn match:
match = cmap matchesA . alignments
defn xmatch:
xmatch s = cmap (unify s) . match
defn xmatchesA:
xmatchesA s = cmap (unify s) . matchesA
cmap after cmap:
cmap f . cmap g = cmap (cmap f . g)
The last, purely combinatorial law is new; we leave verification as an exercise. The calculator produces:
xmatch s

=
{defn xmatch}

cmap (unify s) . match

=
{defn match}

cmap (unify s) . cmap matchesA . alignments

=
{cmap after cmap}

cmap (cmap (unify s) . matchesA) . alignments

=
{defn xmatchesA}

cmap (xmatchesA s) . alignments

So far, so good. That leaves us with the two remaining members of the quartet,
xmatches
and
xmatchesA
. In each case we want to obtain recursive definitions, ones that do not involve
unify
. The two functions are defined in a very similar way, and it is likely that any calculation about one can be adapted immediately to the other. This kind of meta-calculational thought is, of course, beyond the reaches of the calculator.

Let us concentrate on
xmatchesA
. We first make
xmatchesA
entirely pointless, removing the parameter
s
in the definition above. The revised definition is:
xmatchesA :: (Subst,[(Atom,Expr)]) -> Subst

xmatchesA = cup . (one * matchesA)

cup = cmap unify . cpp

where the combinator
cpp
is defined by

cpp (xs,ys) = [(x,y) | x <- xs, y <- ys]

Thus

xmatchesA (sub,aes)

= cup ([sub],aes)

= concat [unify (s,ae) | s <- [sub],ae <- matchesA aes]

= concat [unify (sub,ae) | ae <- matchesA aes]

Apart from the fact that
unify
is now assumed to be a non-curried function, this is a faithful rendition of the definition of
xmatchesA
in pointless form.

The new function
cup
has type
[Subst] -> [Subst] -> [Subst]
. Later on we will exploit the fact that
cup
is an associative function, something that
unify
could never be (why not?). As we saw in
Chapter 7
the accumulating parameter technique depends on the operation of interest being associative.

The first thing to check is that the previous calculation is still valid with the new definitions. Suppose we set up the laws
defn match:
match = cmap matchesA . alignments
defn xmatch:
xmatch = cup . (one * match)
defn xmatchesA:
xmatchesA = cup . (one * matchesA)
The calculator then produces

xmatch

=
{defn xmatch}

cup . (one * match)

=
{defn match}

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

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

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