\documentclass[10pt,twocolumn]{article}

\addtolength{\textheight}{2.4cm}
\addtolength{\hoffset}{-0.8cm}
\addtolength{\voffset}{-2cm}
\addtolength{\textwidth}{1.0cm}

\usepackage{xcolor}
% \usepackage{pgf}
\usepackage{tikz}
\usepackage{representations}

%include polycode.fmt 
%format |-      = "\vdash"
%format Not     = "\neg"
%format :&&:    = "\land"
%format :||:    = "\lor"
%format :->:    = "\to"
%format :<->:   = "\leftrightarrow"
%format :~>:    = "\rightsquigarrow"
%format :+:     = "\nearrow"
%format <*>   = "\ \langle*\rangle\ "
%format <$>   = "\ \langle\$\rangle\ "

\title{Testing a generic term rewrite framework}
\author{Chris Eidhof, Sebastiaan Visser}
\date{\today}
\begin{document}

\maketitle

\abstract{
Automated testing using QuickCheck is a useful addition to Haskell's type
system. Both can be used to state important properties of code.  Manually
producing test data when dealing with a generic library defeats the purpose of
generic programming We show how generic programming can be used to avoid the
boilerplate burden of automated testing.

}

% -----------------------------------------------------------------------------

\section*{Introduction}

As part of the ongoing research on generic programming at the Center for
Software Technology a framework has been designed for generic term rewriting in
Haskell. This framework allows users to define rules which declare domain
specific semantic equivalences. These rules can be used to automatically
rewrite abstract syntax trees for arbitrary domains.

This paper starts by giving a simple introduction to the usage of the
framework. This is accompanied by a simple problem domain we use throughout the
entire paper. The second chapter describes some possible problems that can
arise when using the framework. The third chapter sketches how to prevent these
problems by using automated testing using QuickCheck \cite{quickcheck}. In the fourth chapter we
show how to implement a generic version of QuickCheck's arbitrary function.
This function significantly decreases the amount of work that has to be done in
order to use automated testing.

\section{Rewriting Expression}

We can easily illustrate the use of this framework by means of an example.
Suppose that we are writing an interpreter or compiler for a simple logical
expression language. The data type for our expression language consists out of
constructors for the constants \emph{true} and \emph{false}, the binary
operations for the logical \emph{and}, \emph{or}, \emph{implication} and
\emph{bi-implication}, the \emph{negation} and \emph{variables}:

>data Logic =
>     T
>  |  F
>  |  Logic :&&:   Logic
>  |  Logic :||:   Logic
>  |  Logic :->:   Logic
>  |  Logic :<->:  Logic
>  |  Not Logic
>  |  Var String

Using this data type it is possible to express all sorts of logical statements:

>(Var "x" :->: F) :&&: (Not T :||: Var "y")
>
>(T :<->: F) :->: (F :->: Var "x") :&&: T
>
>(F :||: T) :->: (T :||: F)

An evaluation function together with an variable environment can be used to
reduce these expressions to a single truth value. The following example shows
how to evaluate a logical statement using an simple environment.

> expr = (Var "x" :->: F) :&&: (Not T :||: Var "y")
>
> eval [("x", False), ("y", True)] expr == True

\subsection{Rewrite rules}

Before the semantic interpretation of an expression it might be desirable to
perform some rewriting of the terms first. In general, term rewriting can be
used for several purposes. Dependent on the problem domain terms can be
rewritten in order to optimize, normalize or simplify the interpretation. As a
practical example, most modern compilers perform lots of rewrite rules to the
input program in order to simplify the compilation and produce efficient
machine code.

The rewrite framework allows us to express these rules and apply them to our
syntax trees. In order to demonstrate this, we show how to express three simple
logical equivalence rules. The first rule is the elimination of double
negations, the second and third are the well known De Morgan rules for
\emph{or} and \emph{and} respectively:

> notNot       x     = Not (Not x)     |- x
> deMorganOr   x y   = Not (x :||: y)  |- Not x :&&: Not y
> deMorganAnd  x y   = Not (x :&&: y)  |- Not x :||: Not y

Note how this code is the actual Haskell code -- and the \emph{only} Haskell
code -- that is needed to express these rules. The functions that express the
rules are parametrized with the meta-variables that connect the left hand side
with the right hand sides of the rule. The turnstile symbol ($\vdash$) can be
seen as the infix constructor for rules, taking two semantically equivalent
expressions. 

\subsection{Rewrite function}

To apply these rules the framework offers the function |rewrite|. This function
takes a rule and a term and rewrites the term using the rule. When the term
does not match the rule's left hand side the rewritten term equals the original.

>rewrite :: PFView a => Rule a -> a -> a

The term will only be rewritten on the top level, it does not decent into the
term for deep application. To perform deep rewriting of terms the framework
offers the ability to express rewrite strategies. The explanation of strategies
is outside the scope of this paper.

\subsection{Representation}

So we can use the rewrite framework to easily apply term rewrite rules to our
logical expression data type. The power of the framework can not only be found
in ease of use, but also in the fact that it can be used for \emph{any} data
type. It uses generic programming to abstract over types.

Because standard Haskell does not allow reflection over data types we have to
supply the framework with a representation of our data type manually. We can
get a rich set functions for free when we create a \emph{generic view}, but
creating such a view can be a tedious task. This can be illustrated with the
clumsy piece of code in Figure \ref{logicrep}.

\begin{figure*}
\centering
\small
>instance PFView Logic where
>
>  type PF Logic =
>    C (Sum  (Sum  (Sum (Con (K String))    (Con (Prod Id Id)))
>                  (Sum (Con (Prod Id Id))  (Con (Prod Id Id))))
>            (Sum  (Sum (Con (Prod Id Id))  (Con Id))
>                  (Sum (Con Unit)          (Con Unit))))
>
>  from (Var x)      = C (Inl  (Inl  (Inl  (Con "Var"  (K x)))))
>  from (p :<->: q)  = C (Inl  (Inl  (Inr  (Con "<->"  (Prod (Id p) (Id q))))))
>  from (p :->: q)   = C (Inl  (Inr  (Inl  (Con "->"   (Prod (Id p) (Id q))))))
>  from (p :&&: q)   = C (Inl  (Inr  (Inr  (Con "&&"   (Prod (Id p) (Id q))))))
>  from (p :||: q)   = C (Inr  (Inl  (Inl  (Con "||"   (Prod (Id p) (Id q))))))
>  from (Not p)      = C (Inr  (Inl  (Inr  (Con "Not"  (Id p)))))
>  from T            = C (Inr  (Inr  (Inl  (Con "T"    Unit))))
>  from F            = C (Inr  (Inr  (Inr  (Con "F"    Unit))))
>
>  to (C (Inl  (Inl  (Inl  (Con _ (K x))))))                 = Var x
>  to (C (Inl  (Inl  (Inr  (Con _ (Prod (Id p) (Id q)))))))  = p :<->: q
>  to (C (Inl  (Inr  (Inl  (Con _ (Prod (Id p) (Id q)))))))  = p :->: q
>  to (C (Inl  (Inr  (Inr  (Con _ (Prod (Id p) (Id q)))))))  = p :&&: q
>  to (C (Inr  (Inl  (Inl  (Con _ (Prod (Id p) (Id q)))))))  = p :||: q
>  to (C (Inr  (Inl  (Inr  (Con _ (Id p))))))                = Not p
>  to (C (Inr  (Inr  (Inl  (Con _ Unit)))))                  = T
>  to (C (Inr  (Inr  (Inr  (Con _ Unit)))))                  = F
\caption{The structural representation for the |Logic| data type}
\label{logicrep}
\end{figure*}

This representation uses a common method in generic programming; the data type
will be represented by making the sums, products, constructor names and
fixed points explicit. The framework uses \emph{type families} to express the
relation between the original type and the structural type. In this case the
data type |Logic| and the structural representation |PF Logic|. The functions
|from| and |to| form a so called \emph{embedding projection pair}.  This pair
can be used to convert values in the real world to and from the representation
world.

\section{Problems}

Up till now we have introduced a generic term rewrite framework and
demonstrated how to use this for a simple logical expression language. Because
of the generality of the framework the usage was very simple. Despite this
simplicity, things can go wrong that the compiler will not notice. We isolate
three possible issues:

\begin{itemize}
\item
The rewrite function works on every data type, this means the implementation
must be very precise. How do we ensure that the algorithm is correct?

\item
For every data type that we want to apply a generic function to, we have to
create a structural representation by hand. From the types of the
representation we can easily see that the compiler cannot ensure us that there
are no mistakes in the definition. How do we ensure that the representation is
sound and complete? Can we check that the embedding projection pair forms a
true isomorphism?

\item
When we rewrite a term using a rule we always assume that the semantics of the
value do not change. How can we be sure that every rewrite rule is sound with
respect to the semantics of the problem domain? In our case, are the left and
right hand side of a rule semantically equivalent?
\end{itemize}

These three problems are very hard to tackle using Haskell's type system. We
have to find another way of ensuring ourselves the framework is applied
correctly.

\section{Testing}

Our solution to these potential problems is testing. We use QuickCheck to
automatically test the three properties. We can define a QuickCheck property
for all three problems and this way make sure the framework is used properly.

QuickCheck uses the |arbitrary| type class to create random instances of data
types as input for the tested properties. An instances for the |arbitrary|
class must to be specified for every data type you wish to test for.

Because we are dealing with a generic rewrite framework it would be rather
disappointing when users have to implement their |arbitrary| instances
manually. This is why we have chosen to generate these instance automatically
using a generic arbitrary function. This generic function can rely on the same
structural representation as the generic rewrite function.

\subsection{Rewrite property}

The rewrite property is used to test the correctness of the |rewrite| function.
The property takes a rule and tests whether the rule is correctly applied to a
random term. The term is randomly generated using the |arbitrary| class. The
property plugs this term into the rule, rewrites the left hand side of the rule
and compares this for equality with the right hand side of the rule.

>prop_rewrite :: PFView a => Rule a -> a -> Bool
>prop_rewrite rule a =
>  rewrite rule (lhsR (rule a)) == rhsR (rule a)

To test whether the rewrite algorithm works for the double negation rule we can
write this:

>quickCheck (prop_rewrite notNot)

Unfortunately there is currently no way to generate random rules in order to
automate testing the rewrite property. For now it is sufficient to set up a
number of test cases for some interesting rules. When the rewrite algorithm is
implemented correctly, this test -- together with all other instances of this
test -- should pass.

\subsection{View soundness}

As explained above, the user of the framework should manually supply a
structural representation for their data type together with an embedding
projection pair. Writing these instance becomes a real pain when data types
grow bigger. Accidentally swapping a left projection with right projection in
one of the arms of the embedding projection pair will not be noticed by the
compiler and can cause serious problems.

The following property should check the soundness of the |from| and |to|
functions by checking whether they form the identity:

>prop_fromTo_Id :: PFView a => PF a -> Bool
>prop_fromTo_Id a = (from . to) a == a

It is tempting to think that we could easily check for completeness by testing
the isomorphism the other way around:

>prop_toFrom_Id :: PFView a => a -> Bool
>prop_toFrom_Id a = (to . from) a == a

Actually -- in our framework -- this function will \emph{not} do the expected
job. Because we generate the instances generically using the structural
representation we are trying to test, the test depends on features we are
currently testing! It is easy to see that without true reflection on data types
generically testing for completeness is impossible. We might solve this problem
in the future by automatically generating instances using techniques like
Generic Haskell \cite{gh} or Scrap Your Boilerplate \cite{LPJ03}.

As an example, the following QuickCheck property checks the soundness of the
embedding projection pair for the |Logic| data type. When defined properly this
test should pass.

>quickCheck (prop_fromTo_Id :: PF Logic -> Bool)

\subsection{Semantic soundness}

In order to test the semantic soundness of user defined rules we apply a trick
quite similar to the one for the rewrite algorithm. Given a specific rule and a
random term we fill in the meta-variable of the rule with this term. Now we
rewrite the rule's left hand side and compare this for semantic equality with
the right hand side. The property depends on a user defined function to test
for domain specific semantic equivalence.

>prop_semantics :: PFView a =>
>  (a -> a -> Bool) -> Rule a -> a -> Bool
>prop_semantics eq rule a =
>  let lhs = lhsR (rule a)
>  in maybe False (eq lhs) (rewriteM rule lhs)

To demonstrate the usage of this property we give a specific instance of this
property for the logical expression data type. This property check whether the
original term and the rewritten term evaluate to the same value.

>prop_logicSemantics :: Rule Logic -> Logic -> Bool
>prop_logicSemantics = prop_semantics eqLogic
>  where eqLogic a b = eval a == eval b

As an example, the following property should pass for all instances of |x|.

>quickCheck
> $ prop_logicSemantics (\x -> x :||: Not x |- T))

% -----------------------------------------------------------------------------

\section{Arbitrary instances}

[todo? something like: now that we have defined what has to be tested, ... ]

To use QuickCheck when testing properties, an instance of
Arbitrary has to be provided for every data type that is used. We will take a
look at how this instance is defined for a data type and then give a generic
algorithm to calculate them.

\begin{figure*}
\centering

> data Tree a     =  Leaf a 
>                 |  Branch (Tree a) (Tree a)
> 
\caption{The |Tree| data type}
\label{treedt}

\end{figure*}

First, let us look at the |Tree| data type in Figure \ref{treedt}. There is a
non-recursive constructor |Leaf| and a recursive constructor |Branch| that has
two fixed points, i.e. it recurses twice. The instance for |Arbitrary| is defined
as following:

\begin{spec}
instance Arbitrary a => Arbitrary (Tree a) where
  arbitrary = sized arbTree

arbTree 0  =  Leaf <$> arbitrary
arbTree n  =  frequency
  [  (1  ,  Leaf    <$>  arbitrary  )
  ,  (3  ,  Branch  <$>  arbTree    (n `div` 2) 
                    <*>  arbTree    (n `div` 2)) ]
\end{spec}

The first thing to notice here is that we give a |sized| instance. This is
necessary for termination. If our size is |0|, we only generate the
non-recursive value |Leaf|. If the size is larger than |0|, we give each
constructor a weight of |1| plus the number of fixed points. Second, in the recursive
call, we divide the size by the number of fixed points for that constructor. This
way, the sized value will continue to decrease when recursing.

\subsection{Arbitrary instances: generically}

There are several aspects of the algorithm to calculate these instances
generically. First, because our data types are represented as sums of products,
we have to make the decision at every |Sum|. To get the frequencies for this
decision, we have to synthesize the weights for both the left and the right
subtree. Second, when recursing, we want to decrease the size by dividing it by
the number of fixed points in the current constructor. This is number is also
calculated in the |Sum| and passed on using the |divisor| field of |ArbParams|.

\begin{figure*}
\centering
\begin{code}
garbitrary' params size  =  frequency 
  [(  fr fpl  ,  Inl   <$> garbitrary' params {divisor = sum fpl  } size)
  ,(  fr fpr  ,  Inr   <$> garbitrary' params {divisor = sum fpr  } size)
  ]
  where  
    (Node fpl fpr)  =   gfixpoints' (undefined :: Sum f g a)
    fr  ::  Tree Int -> Int
    fr  =   sum . fmap (freq size)
    freq  0  0  =  1 
    freq  0  _  =  0
    freq  _  x  =  x + 1
\end{code}
\caption{The function |garbitrary'| for the |GArbitrary| instance of |Sum f g|.}
\label{arbsum}
\end{figure*}

In Figure \ref{arbsum}, we see the code for the instance of |GArbitrary| for
|Sum|. We call the |frequency| function with a list of two pairs, one for the
|Inl| and one for the |Inr|. The first component of the pair is the
frequency for that constructor, the second component is the recursive call for
that sub-value. To calculate the frequency, we first calculate a binary tree that
contains all the fixed points for every constructor, which has the same shape as
the structural representation. The function |fr| calculates the frequency based
on the size and the number of fixed points. If the size is |0|, it will only give
non-recursive constructors a chance, otherwise we add |1| to the number of
fixed points.

There is one other interesting case for |GArbitrary|, and that is |Id|, which
captures the recursion. Here we make use of the |ArbParams| data type, and use
both the recursive call |r| and the divisor |d|:

\begin{code}
instance GArbitrary Id where
  garbitrary' p@(AP r d) size =
    Id <$> r p (size `div` d)
\end{code}

For the full code of |GArbitrary|, see appendix~\ref{sec:garbitrary}.

\subsection{Calculating the fixed points}

For |garbitrary|, we need a tree of fixed points. Using the generic framework, we
can calculate this. Our fixed points are stored in a binary tree with values at the
leafs, just as in Figure~\ref{figure:treedt}.

As an example, we want to calculate the fixpoint-tree for the |Direction|
data type:

> data Direction  =  North  |  East
>                 |  South  |  West
>                 |  Direction :+: Direction

The structural representation looks like this:

> type PF Direction =
>       Sum  Unit 
>            (Sum  Unit 
>                  (Sum  Unit 
>                        (Sum Unit (Prod Id Id))))

There are two fixed points in the |:+:| constructor, and that is reflected in the
structural representation by |Prod Id Id|. We can see the outcome of our
algorithm in Figure~\ref{directiongraph}.

\begin{figure*}
\centering
\directionfixedpoints
\caption{The fixed-point graph for |Direction|}
\label{directiongraph}
\end{figure*}

Our class for calculating the fixed points looks like this:

> class GFixpoints f where
>   gfixpoints' :: f a -> Tree Int

The value |f a| is never used directly in our instances, but is only provided so
we can give inline types to our recursive calls, as we will see in the instance
for |Sum|.

For |Unit| and |K|, we return a singleton tree with |0| as the value. For the
recursive calls, however, we need to return |1|:

> instance GFixpoints Id where
>   gfixpoints' _ = Leaf 1

For sum, we use |undefined| to make sure the recursive calls are on the
components of |Sum|. In |garbitrary|, this is where we need to choose, so that
is why we branch our tree here using |Node|.

> instance (  GFixpoints f, GFixpoints g) => 
>             GFixpoints (Sum f g) where
>   gfixpoints' _ =  gfixpoints' (undefined :: f a  )
>            `Node`  gfixpoints' (undefined :: g a  )

For |Prod|, we need to sum the values for both components. In the case of
direction, we have a |Prod Id Id|. Calculating an |Id| value will return a |Leaf
1|, and here we sum them to get a |Leaf 2|.
 
> instance (  GFixpoints f, GFixpoints g) =>
>             GFixpoints (Prod f g) where
>   gfixpoints' _ = (+)  <$>  gfixpoints' (undefined :: f a  )
>                        <*>  gfixpoints' (undefined :: g a  )

The full code for the GFixpoints module is in appendix~\ref{sec:gfixpoints}

\section{Conclusion}

We have seen how we can test our rewriting framework on the correctness of the
rewriting algorithm, how we can test our embedding projection pairs on soundness
and how we can test the rewriting rules on semantic equality. In order to do
this, we have shown a generic algorithm for creating QuickCheck instances.

While we can currently only check for soundness of the embedding projection
pairs, we would ideally also test for completeness. This could be done by
introspection on the data type by, for example, using the Scrap Your Boilerplate
approach that is integrated in GHC. Alternatively we could use Template Haskell,
but the current implementation of Template Haskell does not support type
families.

We now have a powerful test framework that will catch a lot of mistakes,
automatically. For users of this test framework, a minimal amount of work has to
be done. They only have to make sure they test their rules with
|prop_semantics|.

\section*{Acknowledgements}

We would like to thank the teachers and fellow students of the Generic
Programming course for the fun and insightful discussions during the course.
Also, Alexey Rodriguez deserves special mentioning, without his help and
encouragement this paper would not have been possible.

\bibliography{paper}
\bibliographystyle{plain}

\pagebreak

\section*{Appendices}

\appendix

\section{Module GArbitrary}
\label{sec:garbitrary}

\begin{code}
instance Applicative Gen where
  (<*>)  =  ap
  pure   =  return

data ArbParams a = AP {
     rec      ::  ArbParams a -> Int -> Gen a
  ,  divisor  ::  Int
  }

class GArbitrary f where
  garbitrary'    ::  ArbParams a -> Int -> Gen (f a)

instance GArbitrary Unit where
  garbitrary' _ _ = pure Unit

instance GArbitrary Id where
  garbitrary' p@(AP r d) t = Id <$> r p (t `div` d)

instance Arbitrary a => GArbitrary (K a) where
  garbitrary' _ _ = K <$> arbitrary

instance (  GFixpoints f,  GFixpoints g,
            GArbitrary f,  GArbitrary g) =>
            GArbitrary (Sum f g) where
  garbitrary' p s   =  frequency [rec fpl Inl, rec fpr Inr]
    where
      rec a b =
        (fr a, b <$> garbitrary' p {divisor = sum a} s)
      (Node fpl fpr)  = gfixpoints' (undefined :: Sum f g a)
      fr       = foldTree (f s) (+)
      f  0  0  =  1
      f  0  _  =  0
      f  _  x  =  x + 1

instance (GArbitrary f, GArbitrary g) =>
          GArbitrary (Prod f g) where
  garbitrary' p s = Prod <$>
    garbitrary' p s <*> garbitrary' p s

instance GArbitrary f =>
  GArbitrary (Con f) where
  garbitrary' p s = Con "" <$> garbitrary' p s

instance GArbitrary f =>
  GArbitrary (C f) where
  garbitrary' p s = C <$> garbitrary' p s

garbitrary :: (GArbitrary (PF a), PFView a) =>
  Int -> Gen a
garbitrary s = garbitraryHelper (AP undefined 1) s

garbitraryHelper ::
  (PFView a, GArbitrary (PF a)) => 
  ArbParams a -> Int -> Gen a
garbitraryHelper p s = to <$>
  garbitrary' p {rec = garbitraryHelper} s
\end{code}

\section{Module GFixpoints}
\label{sec:gfixpoints}
\begin{code}
module GFixpoints where

data Tree a = Leaf a | Node (Tree a) (Tree a)
 deriving Show

instance Applicative Tree where
  pure = Leaf
  Leaf x <*> Leaf y = Leaf (x y)
  -- partial instance

foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
foldTree l n (Leaf x)    = l x
foldTree l n (Node x y)  =
  (foldTree l n x) `n` (foldTree l n y)

sum :: Tree Int -> Int
sum = foldTree id (+)

instance Functor Tree where
  fmap f = foldTree (Leaf . f) Node

class GFixpoints f where
  gfixpoints' :: f a -> Tree Int

instance GFixpoints Unit where
  gfixpoints' _ = Leaf 0

instance GFixpoints Id where
  gfixpoints' _ = Leaf 1

instance GFixpoints (K a) where
  gfixpoints' _ = Leaf 0

instance (GFixpoints f, GFixpoints g) =>
  GFixpoints (Sum f g) where
  gfixpoints' _ =
     gfixpoints' (undefined :: f a) `Node` gfixpoints' (undefined :: g a)

instance ( GFixpoints f, GFixpoints g) =>
           GFixpoints (Prod f g) where
  gfixpoints' _ = (+)  <$> gfixpoints' (undefined :: f a)
                       <*> gfixpoints' (undefined :: g a)

instance GFixpoints f => GFixpoints (Con f) where
  gfixpoints' _ = gfixpoints' (undefined :: f a)

\end{code}

\end{document}