Approx is a class for approximation functions as described
in The generic approximation lemma, Graham Hutton and Jeremy
Gibbons, Information Processing Letters, 79(4):197-201, Elsevier
Science, August 2001, http://www.cs.nott.ac.uk/~gmh/bib.html.
Instances are provided for all members of the Data type class. Due
to the limitations of the Data.Generics approach to generic
programming, which is not really aimed at this kind of application,
the implementation is only guaranteed to perform correctly, with
respect to the paper (and modulo any bugs), on non-mutually-recursive
sum-of-products datatypes. In particular, nested and mutually
recursive types are not handled correctly with respect to the
paper. The specification below is correct, though (if we assume that
the Data instances are well-behaved).
In practice the approxAll function can probably be more useful than
approx. It traverses down all subterms, and it should be possible
to prove a variant of the approximation lemma which approxAll
satisfies.
|