Thinking Functionally with Haskell (50 page)

reverseCalc (Calc e steps)

= foldl shunt (Calc e []) steps

where shunt (Calc e1 steps) (why,e2)

= Calc e2 ((why,e1):steps)

In order to paste two calculations together we first have to check that their conclusions are the same. If they are not, then we go ahead and paste the calculations anyway with an indication of failure:
conc1

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

conc2

If the two conclusions are the same, we can be a little smarter than just stitching the calculations together. If the penultimate conclusion of one calculation also matches the penultimate conclusion of the other, then we can cut out the final steps altogether. And so on. Here, then, is how we paste two calculations:
paste :: Calculation -> Calculation -> Calculation

paste calc1@(Calc e1 steps1) calc2

= if conc1 == conc2

then Calc e1 (prune conc1 rsteps1 rsteps2)

else Calc e1 (steps1 ++ (gap,conc2):rsteps2)

where Calc conc1 rsteps1 = reverseCalc calc1

Calc conc2 rsteps2 = reverseCalc calc2

gap = "... ??? ..."

The function
prune
is defined by:

prune :: Expr -> [Step] -> [Step] -> [Step]

prune e ((_,e1):steps1) ((_,e2):steps2)

| e1==e2 = prune e1 steps1 steps2

prune e steps1 steps2 = rsteps ++ steps2

where Calc _ rsteps = reverseCalc (Calc e steps1)

Finally, here is the module declaration of
Calculations
:

module Calculations

(Calculation (Calc), Step, calculate, paste)

where

import Expressions

import Laws

import Rewrites

import Utilities (compose)

The exports are those types and functions needed to define
simplify
and
prove
in the main module.

The sole purpose of the module
Rewrites
is to provide a definition of the function
rewrites
that appears in the definition of
calculate
. Recall that the expression
rewrites eqn e
returns a list of all expressions that can arise by matching some subexpression of
e
against the left-hand expression of
eqn
and replacing the subexpression with the appropriate instance of the right-hand expression of
eqn
.

The fun is in figuring out how to define
rewrites
. Suppose we construct a list of all possible subexpressions of an expression. We can match the given equation against each subexpression, get the substitutions that do the matching (of which there may be none, one or more than one; see the section on matching below) and compute the new subexpressions. But how do we replace an old subexpression with a new one in the original expression? The simple answer is that we can’t, at least not without determining alongside each subexpression its
context
or
location
in the original expression. The new subexpression can then be inserted at this location.

Rather than introducing contexts explicitly, we take another approach. The idea is to burrow into an expression, applying a rewrite to some subexpression at some point, and then to build the rewritten expression as we climb back out of the burrow. We will need a utility function
anyOne
that takes a function yielding a choice of alternatives, and a list, and installs a single choice for one of the elements. The definition is
anyOne :: (a -> [a]) -> [a] -> [[a]]

anyOne f []
= []

anyOne f (x:xs) = [x':xs | x' <- f x] ++

[x:xs' | xs' <- anyOne f xs]

For example, if
f 1 = [-1,-2]
and
f 2 = [-3,-4]
, then
anyOne f [1,2] = [[-1,2],[-2,2],[1,-3],[1,-4]]

Either one of the choices for the first element is installed, or one of the choices for the second, but not both at the same time.

Here is our definition of
rewrites
:

rewrites :: Equation -> Expr -> [Expr]

rewrites eqn (Compose as) = map Compose (

rewritesSeg eqn as ++ anyOne (rewritesA eqn) as)

rewritesA eqn (Var v) = []

rewritesA eqn (Con k es)

= map (Con k) (anyOne (rewrites eqn) es)

In the first line we concatenate the rewrites for a
segment
of the current expression with the rewrites for any one of its proper subexpressions. Only constants with arguments have subexpressions. Note that the two uses of
anyOne
have different types, one taking a list of atoms, and one taking a list of expressions.

It remains to define
rewritesSeg
:

rewritesSeg :: Equation -> [Atom] -> [[Atom]]

rewritesSeg (e1,e2) as

= [as1 ++ deCompose (apply sub e2) ++ as3

| (as1,as2,as3) <- segments as,

sub <- match (e1,Compose as2)]

The function
segments
splits a list into segments:

segments as = [(as1,as2,as3)

| (as1,bs) <- splits as,

(as2,as3) <- splits bs]

The utility function
splits
splits a list in all possible ways:
splits :: [a] -> [([a],[a])]

splits []
= [([],[])]

splits (a:as) = [([],a:as)] ++

[(a:as1,as2) | (as1,as2) <- splits as]

For example,

ghci> splits "abc"

[("","abc"),("a","bc"),("ab","c"),("abc","")]

The remaining functions
apply
and
match
have types
apply :: Subst -> Expr -> Expr

match :: (Expr,Expr) -> [Subst]

Each will be defined in their own modules,
Substitutions
and
Matchings
. Finally, here is the module declaration for
Rewrites
:
module Rewrites (rewrites)

where

import Expressions

import Laws (Equation)

import Matchings (match)

import Substitutions (apply)

import Utilities (anyOne, segments)

The sole purpose of the module
Matchings
is to define the function
match
. This function takes two expressions and returns a list of substitutions under which the first expression can be transformed into the second. Matching two expressions produces no substitutions if they don’t match, but possibly many if they do. Consider matching the expression
foo (f . g)
against
foo (a . b . c)
. There are four substitutions that do the trick:
f
may be bound to any of the expressions
id, a, a . b, a . b . c

with four corresponding bindings for
g
. Although the calculator will select a single substitution at each step, it is important to take account of multiple substitutions in the process of obtaining the valid matchings. For example, in matching
foo (f . g) . bar g
against
foo (a . b . c) . bar c
, the subexpression
f . g
is matched against
a . b . c
, resulting in four possible substitutions. Only when
bar g
is matched against
bar c
are three of the substitutions rejected. A premature commitment to a single substitution for the first match may result in a successful match being missed.

The most straightforward way of defining
match (e1,e2)
is to first line up the atoms of
e1
with a partition of the atoms of
e2
; the first atom is associated with the first segment of the partition, the second with the second segment, and so on. The function
alignments
has type
alignments :: (Expr,Expr) -> [[(Atom,Expr)]]

and does the alignments. To define it we need a function
parts
that partitions a list into a given number of segments:
parts :: Int -> [a] -> [[[a]]]

parts 0 [] = [[]]

parts 0 as = []

parts n as = [bs:bss

| (bs,cs) <- splits as,

bss <- parts (n-1) cs]

The interesting clauses are the first two: there is one partition of the empty list into 0 segments, namely the empty partition, but there are no partitions of a nonempty list into 0 segments. For example,
ghci> parts 3 "ab"

[["","","ab"],["","a","b"],["","ab",""],

["a","","b"],["a","b",""],["ab","",""]]

Now we can define

alignments (Compose as,Compose bs)

= [zip as (map Compose bss) | bss <- parts n bs]

where n = length as

Having aligned each atom with a subexpression, we define
matchA
that matches atoms with expressions:
matchA :: (Atom,Expr) -> [Subst]

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

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

| k1==k2 = combine (map match (zip es1 es2))

matchA _ = []

Matching a variable always succeeds and results in a single substitution. Matching two constants succeeds only if the two constants are the same. In all other cases
matchA
returns an empty list of substitutions. The function
matchA
depends on
match
, which we can now define by
match :: (Expr,Expr) -> [Subst]

match = concatMap (combine . map matchA) . alignments

The final ingredient is the function
combine :: [[Subst]] -> [Subst]
. Each component list of substitutions in the argument of
combine
represents alternatives, so
combine
has to combine alternatives by selecting, in all possible ways, one substitution from each list and then unifying the result. We will return to this function in the module for substitutions. This completes the definition of
matches
. The module declaration is
module Matchings (match)

where

import Expressions

import Substitutions (Subst, unitSub, combine)

import Utilities (parts)

We place
parts
in the utilities module because it is not specific to expressions.

A substitution is a finite mapping associating variables with expressions. A simple representation as an association list suffices:
type Subst = [(VarName,Expr)]

The empty and unit substitutions are then defined by

emptySub = []

unitSub v e = [(v,e)]

We can apply a substitution to an expression to get another expression by defining

apply :: Subst -> Expr -> Expr

apply sub (Compose as)

= Compose (concatMap (applyA sub) as)

applyA sub (Var v) = deCompose (binding sub v)

applyA sub (Con k es) = [Con k (map (apply sub) es)]

The function
binding
looks up a nonempty substitution for the binding for a variable:
binding :: Subst -> VarName -> Expr

binding sub v = fromJust (lookup v sub)

The function
lookup
is supplied in the Haskell Prelude and returns
Nothing
if no binding is found, and
Just e
if
v
is bound to
e
. The function
fromJust
is in the library
Data.Maybe
and removes the wrapper
Just
.

Next we tackle
combine
. This function has to combine alternative substitutions by selecting, in all possible ways, one substitution from each component list and then unifying each resulting list of substitutions:
combine = concatMap unifyAll . cp

The utility function
cp
, which we have seen many times before, computes the cartesian product of a list of lists.

The function
unifyAll
takes a list of substitutions and unifies them. To define it we first show how to unify two substitutions. The result of unification is either the union of the two substitutions if they are compatible, or no substitution if they are incompatible. To handle the possibility of failure, we can use the
Maybe
type, or simply return either an empty list or a singleton list. We choose the latter simply because in the following section we are going to calculate another version of the calculator, and it is simplest to stick with list-based functions:
unify :: Subst -> Subst -> [Subst]

unify sub1 sub2 = if compatible sub1 sub2

then [union sub1 sub2]

else []

In order to define
compatible
and
union
we will suppose that substitutions are maintained as lists in lexicographic order of variable name. Two substitutions are incompatible if they associate different expressions with one and the same variable:
compatible [] sub2 = True

compatible sub1 [] = True

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

| v1