Generating Generic Functions
Alexey
Johan Jeuring, Alexey Rodriguez and Gideon Smeding. At the ACM SIGPLAN Workshop on Generic Programming 2006
We present an approach to the generation of generic functions from
user-provided specifications. The specifications consist of the type
of a generic function, examples of instances that it should "match"
when specialized, and properties that the generic function should satisfy.
We use the type-based function generator Djinn to generate terms for
specializations of the generic function types on the type indices of
generic functions. Then we use QuickCheck to prune the generated
terms by testing against properties, and by testing specialized candidate
functions against the provided examples. Using this approach we have
been able to generate generic equality, map, and zip functions,
for example.
Paper: (
pdf)
Technical report: (
url)
Software
Our implementation uses
Djinn to generate the components of a generic function. To find the right components among the generated candidates we use
QuickCheck for checking their validity against specific properties. This requires the evaluation of candidate terms. For their evaluation we did as follows: first we convert untyped expressions (normal data types) into typed expressions (GADTs); then, we evaluate the GADTs in the usual "tagless" way. Probably one of the most interesting parts of the implementation is this "typing" of untyped expressions in Haskell.
You can download the source code for the implementation together with Djinn from the following link:
Please read the
README file in the
UU directory for instructions on how to generate generic functions.
In addition to the functions generated for the paper, we can now generate the generic compare function.
Runtime compilation of functional terms
As stated above, the function candidates that are found with Djinn, are discarded/accepted using Softare testing. To that end a term representing a function is transformed to the equivalent function in the host language (Haskell), and testing is performed on it. This provides two advantages, one is easier integration with existing tools (
QuickCheck? ) and under some circumstances if the term is not repeatedly inspected for evaluation, the performance is improved, effectively compiling the term away. You can find below a presentation of these ideas.
Slides : Runtime compilation of functional terms (
pdf)
--
AlexeyRodriguez - 01 Nov 2006
