code-conjure
synthesize Haskell functions out of partial definitions
https://github.com/rudymatela/conjure#readme
LTS Haskell 22.40: | 0.5.14 |
Stackage Nightly 2024-11-06: | 0.5.14 |
Latest on Hackage: | 0.5.14 |
code-conjure-0.5.14@sha256:ee431f3462360efb9733c2d3bf523eded376eda7876d87c8390b7e9e2c6e3bd1,4805
Conjure
Conjure is a tool that synthesizes Haskell functions out of partial definitions.
Installing
To install the latest Conjure version from Hackage, just run:
$ cabal update
$ cabal install code-conjure
Prerequisites are express, leancheck and speculate. They should be automatically resolved and installed by Cabal.
NOTE: the name of the Hackage package is code-conjure
– not to be confused with Conjure the BitTorrent client.
Starting from Cabal v3.0, you need to pass --lib
as an argument to
cabal install
to install packages globally on the default
user environment:
$ cabal install code-conjure --lib
If you already have Conjure installed Cabal may refuse to update to the latest version. To update, you need to reset your user’s cabal installation with:
rm -rf ~/.cabal/{bin,lib,logs,share,store} ~/.ghc/*/
WARNING: the above command will erase all user-local packages.
Synthesizing functions
To use Conjure, import the library with:
import Conjure
Then, declare a partial definition of a function to be synthesized. For example, here is a partial implementation of a function that squares a number:
square :: Int -> Int
square 0 = 0
square 1 = 1
square 2 = 4
Next, declare a list of primitives that seem like interesting pieces in the final fully-defined implementation. For example, here is a list of primitives including addition, multiplication and their neutral elements:
primitives :: [Prim]
primitives = [ pr (0::Int)
, pr (1::Int)
, prim "+" ((+) :: Int -> Int -> Int)
, prim "*" ((*) :: Int -> Int -> Int)
]
Finally, call the conjure
function,
passing the function name, the partial definition and the list of primitives:
> conjure "square" square primitives
square :: Int -> Int
-- testing 3 combinations of argument values
-- pruning with 14/25 rules
-- looking through 3 candidates of size 1
-- looking through 4 candidates of size 2
-- looking through 9 candidates of size 3
square x = x * x
Conjure is able to synthesize the above implementation in less than a second.
For more information, see the eg/arith.hs
example and
the Haddock documentation for the conjure
and conjureWith
functions.
Synthesizing recursive functions
Conjure supports synthetization of recursive functions.
Take for example the following partial implementation of a function that computes the factorial of a number:
factorial :: Int -> Int
factorial 1 = 1
factorial 2 = 2
factorial 3 = 6
factorial 4 = 24
Here is a list of primitives:
primitives :: [Prim]
primitives = [ pr (0::Int)
, pr (1::Int)
, prim "+" ((+) :: Int -> Int -> Int)
, prim "*" ((*) :: Int -> Int -> Int)
, prim "-" ((-) :: Int -> Int -> Int)
]
And here is what Conjure produces with the above partial definition and list of primitives:
> conjure "factorial" factorial primitives
factorial :: Int -> Int
-- testing 4 combinations of argument values
-- pruning with 27/65 rules
-- looking through 3 candidates of size 1
-- looking through 4 candidates of size 2
-- looking through 13 candidates of size 3
-- looking through 34 candidates of size 4
-- looking through 75 candidates of size 5
-- looking through 183 candidates of size 6
-- looking through 577 candidates of size 7
factorial 0 = 1
factorial x = x * factorial (x - 1)
The above synthetization takes less than a second.
It is also possible to generate a folding implementation like the following:
factorial x = foldr (*) 1 [1..x]
by including enumFromTo
and foldr
in the background.
For more information, see the eg/factorial.hs
example and
the Haddock documentation for the conjure
and conjureWith
functions.
Synthesizing from specifications (for advanced users)
Conjure also supports synthesizing from a functional specification
with the functions conjureFromSpec
and conjureFromSpecWith
as, in some cases,
a partial definition may not be appropriate
for one of two reasons:
- Conjure may fail to “hit” the appropriate data points;
- specifying argument-result bindings may not be easy.
Take for example a function duplicates :: Eq a => [a] -> [a]
that should return the duplicate elements in a list without repetitions.
Let’s start with the primitives:
primitives :: [Prim]
primitives = [ pr ([] :: [Int])
, prim "not" not
, prim "&&" (&&)
, prim ":" ((:) :: Int -> [Int] -> [Int])
, prim "elem" (elem :: Int -> [Int] -> Bool)
, prif (undefined :: [Int])
]
Now here’s a first attempt at a partial definition:
duplicates' :: [Int] -> [Int]
duplicates' [] = []
duplicates' [1,2,3,4,5] = []
duplicates' [1,2,2,3,4] = [2]
duplicates' [1,2,3,3,3] = [3]
duplicates' [1,2,2,3,3] = [2,3]
Here is what conjureWith
prints:
> conjureWith args{maxSize=18} "duplicates" duplicates primitives
duplicates :: [Int] -> [Int]
-- testing 1 combinations of argument values
-- pruning with 21/26 rules
-- looking through 2 candidates of size 1
duplicates xs = xs
The generated function clearly does not follow our specification. But if we look at the reported number of tests, we see that only one of the argument-result bindings of our partial definition was used. Conjure failed to hit any of the argument values with five elements. (Since Conjure uses enumeration to test functions these values have to be kept “small”).
Here is a second attempt:
duplicates :: [Int] -> [Int]
duplicates [0,0] = [0]
duplicates [0,1] = []
duplicates [1,0,1] = [1]
Here is what conjureWith
now prints:
> conjureWith args{maxSize=18} "duplicates" duplicates primitives
duplicates :: [Int] -> [Int]
-- testing 3 combinations of argument values
-- pruning with 21/26 rules
-- ...
-- looking through 16 candidates of size 9
duplicates [] = []
duplicates (x:xs) = if elem x xs then [x] else []
The duplicates
function that Conjure generated is still not correct.
Nevertheless, it does follow our partial definition. We have to refine it.
Here is a third attempt with more argument-result bindings:
duplicates :: [Int] -> [Int]
duplicates [0,0] = [0]
duplicates [0,1] = []
duplicates [1,0,1] = [1]
duplicates [0,1,0,1] = [0,1]
Here is what Conjure prints:
duplicates [] = []
duplicates (x:xs) = if elem x xs then x:duplicates xs else []
This implementation follows our partial definition, but may return duplicate duplicates, see:
duplicates [1,0,1,0,1] = [1,0,1]
Here is a fourth and final refinement:
duplicates :: [Int] -> [Int]
duplicates [0,0] = [0]
duplicates [0,1] = []
duplicates [1,0,1] = [1]
duplicates [0,1,0,1] = [0,1]
duplicates [1,0,1,0,1] = [0,1]
duplicates [0,1,2,1] = [1]
Now Conjure prints a correct implementation:
> conjureWith args{maxSize=18} "duplicates" duplicates primitives
duplicates :: [Int] -> [Int]
-- testing 6 combinations of argument values
-- ...
-- looking through 2189 candidates of size 17
duplicates [] = []
duplicates (x:xs) = if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
(in 1.5s)
In this case,
specifying the function with specific argument-result bindings
is perhaps not the best approach.
It took us four refinements of the partial definition to get a result.
Specifying test properties perhaps better describes what we want.
Again, we would like duplicates
to return all duplicate elements
without repetitions.
This can be encoded in a function using holds
from LeanCheck:
import Test.LeanCheck (holds)
duplicatesSpec :: ([Int] -> [Int]) -> Bool
duplicatesSpec duplicates = and
[ holds 360 $ \x xs -> (count (x ==) xs > 1) == elem x (duplicates xs)
, holds 360 $ \x xs -> count (x ==) (duplicates xs) <= 1
] where count p = length . filter p
This function takes as argument a candidate implementation of duplicates
and returns whether it is valid.
The first property states that all duplicates must be listed.
The second property states that duplicates themselves must not repeat.
Now, we can use the function conjureFromSpecWith
to generate the same duplicates function
passing our duplicatesSpec
as argument:
> conjureFromSpecWith args{maxSize=18} "duplicates" duplicatesSpec primitives
duplicates :: [Int] -> [Int]
duplicates [] = []
duplicates (x:xs) = if elem x xs && not (elem x (duplicates xs)) then x:duplicates xs else duplicates xs
(in 1.5s)
For more information see the eg/dupos.hs
example and
the Haddock documentation for the conjureFromSpec
and conjureFromSpecWith
functions.
The functions conjureFromSpec
and conjureFromSpecWith
also accept specifications
that bind specific arguments to results.
Just use ==
and &&
accordingly:
duplicatesSpec :: ([Int] -> [Int]) -> Bool
duplicatesSpec duplicates = duplicates [0,0] == [0]
&& duplicates [0,1] == []
&& duplicates [1,0,1] == [1]
&& duplicates [0,1,0,1] == [0,1]
&& duplicates [1,0,1,0,1] == [0,1]
&& duplicates [0,1,2,1] == [1]
With this, there is no way for Conjure to miss argument-result bindings.
Related work
Conjure’s dependencies. Internally, Conjure uses LeanCheck, Speculate and Express. LeanCheck does testing similarly to QuickCheck, SmallCheck or Feat. Speculate discovers equations similarly to QuickSpec. Express encodes expressions involving Dynamic types.
Program synthesis within Haskell.
MagicHaskeller (2007) is another tool
that is able to generate Haskell code automatically.
It supports recursion through
catamorphisms, paramorphisms and the fix
function.
Igor II (2010) is able to synthesize Haskell
programs as well.
Hoogle (2004) is a search engine for Haskell functions. It is not able to synthesize expressions but it can find functions that match a type. Hoogle+ (2020) is similar to Hoogle but is able to search for small expressions. In addition to the type, Hoogle+ allows users to provide tests that the function should pass.
Program synthesis beyond Haskell.
PushGP (2002) and G3P (2017) are genetic programming systems that are able to synthesize programs in Push and Python respectively. Differently from Conjure or MagicHaskeller, they require around a hundred tests for traning instead of just about half a dozen.
Barliman (2016) for Lisp is another tool that does program synthesis.
Further reading
For a detailed documentation of each function, see Conjure’s Haddock documentation.
The eg
folder in the source distribution
contains more than 60 examples of use.
Conjure, Copyright 2021-2024 Rudy Matela, distribued under the 3-clause BSD license.
Changes
Changelog for (Code) Conjure
v0.5.14 (February 2024)
- improve commutative pruning, slightly faster Conjure
- add
carryOn
,rewriting
,requireDescent
,adHocRedundancy
switches to theArgs
record - add more benchmarks and tests
v0.5.12 (February 2024)
- bump Speculate requirement to v0.4.20
- improve testing of Conjure itself
- improvements and fixes of Conjure’s benchmarks
v0.5.10 (February 2024)
- improve pruning of candidate functions;
Conjure
: un-export experimentalequalModuloTesting
Conjure.Conjurable
: addconjureListFor
,conjureSizeFor
&conjureGrounds
;- Reorganize internal modules
- Add
Conjure.Defn.Redundancy
module for redundant candidates; - Add
Conjure.Defn.Test
module testing candidate definitions; - Add
Conjure.Reason
module for term-rewriting-based reasoning; - Add
Conjure.Red
module for recursive descent; Conjure.Expr
: add a few auxiliary functions- Move functions out of
Conjure.Engine
into new modules - add more examples and benchmarks;
- improved testing of Conjure itself;
- and several other improvements and fixes.
v0.5.8 (January 2024)
- prune redundant mutants using a few new rules
- rework numeric recursion criteria
- improve pretty-printing
- improve error handling
- refactor and lint throughout
- Conjurable tuples up to 12-tuples
- bump Express requirement to v1.0.14 (bugfix)
v0.5.6 (November 2023)
Conjure
module: no main API changesConjure.Engine
: addequalModuloTesting
Conjure.Utils
: add some misc functions- add
bench/redundants
that reports groups of redundant candidates
v0.5.4 (November 2023)
This has been the “dev” version after v0.5.2 for almost a couple of years:
- report invalid theories-from-testing
- weed-out some redundant candidates:
- add and use
isRedundantDefn
- update how deconstructions are handled
- add and use
- add (but not use)
conjureSize
toConjurable
v0.5.2 (March 2022)
- show number of tested candidates
- complete
Conjurable
derivation functions - reference related work on README
- add switch to unique-modulo-testing candidates (slow) to allow computing the near upper/lower limit on pruning
v0.5.0 (September 2021)
- allow synthesizing/conjuring from properties with
conjureFromSpec
; - complete Haddock documentation;
- remove several unused functions;
- add stub
conjurableDerive
functions; - Makefile: add targets to run GPS(2) and TerpreT benches.
v0.4.4 (September 2021)
- remove need for explicit deconstructions:
- use
-
and1
instead ofdec
; - allow
mod
anddiv
as deconstructions;
- use
- bump Express requirement to v1.0.6 (bugfix);
- complete the GPS1 benchmark;
- add GPS2 and TerpreT benchmarks;
- minor fixes in the README.
v0.4.2 (August 2021)
- default to using top-level patterns on generated functions;
- memoize function evaluation;
- double-check theory at the end and report warning on incorrect properties;
- add
prif
toConjure
; - simplify deconstructor discovery and add
conjureSize
toConjurable
; - add
cevaluate
,ceval
andcvl
toConjure.Conjurable
; - add
bench/gps
andbench/lowtests
; - improve tests and benchmarks.
v0.4.0 (July 2021)
- background primitives are now provided with
pr
andprim
. - report number of rules used in pruning
- require Express v1.0.4 and Speculate v0.4.12
- allow
..
notation - add benchmarks, replicate, subset, p12, p30 and candidates
- add and use the
Defn
type andconjureDefns
- minor changes in benchmarks
- cleanup unused code
v0.3.6 (June 2021)
- add switch for descending recursions
to allow generation of
gcd
- refactor recursion generation (replace a hole later)
- change
conjpureWith
to takeArgs
- rename two args fields to
maxBodyRecursions
andmaxEvalRecursions
at this point, the old names were misnomers.
v0.3.4 (June 2021)
- reallow recursions under
&&
and||
(simplifies the generatedor
,and
,set
andelem
functions) - only require deconstructions on a non-empty subset of arguments
(allows
fib01
to be produced) - limit number of terminal evaluations in
recursiveToDynamic
- fix bug in
recursiveToDynamic
(not counting some recursions) - add 4 new benchmarks:
count
,gcd
,tree
andsetelem
v0.3.2 (June 2021)
- significant runtime reduction in several benchmarks, e.g.:
- take is now reachable in about 5 seconds
- improved candidate generation:
- faster runtime
- fewer redundant/invalid candidates
- limit recursive calls to use deconstructors
- test to find deconstructors automatically
- improve recursion evaluation method (
revaluate
replacesrecursexpr
) - add fibonacci benchmark
- minor:
- record runtimes with one decimal place instead of two
- add longshot benchmark
- add intercalate to the list benchmark
- add stub
Conjure.Constructors
module
v0.3.0 (May 2021)
- only automatically include an
if
for the return type of the given function - add the
take-drop
benchmark - make bottom-up enumeration more type directed
v0.2.8 (May 2021)
- export the
A
,B
,C
,D
,E
andF
helper types
v0.2.6 (May 2021)
- require Express v0.1.10 due to
hasHole
being now exported there - require Eq result on
conjure1
,conjure2
andconjure3
- code cleanup and more tests
v0.2.4 (May 2021)
- allow conjuring from specifications in addition to partial definitions
(
conjure1
,conjure2
,conjure3
and related functions) - improve examples
- improve criteria for automatic primitive inclusion:
- only include
if :: ... -> Bool
if there areBool
primitives - include
False
andTrue
automatically only on Speculate’s background
- only include
- add code-optional candidate nubbing and debug functions
v0.2.2 (May 2021)
- by default, search for 60 argument combinations among 100000 enumerated combinations
v0.2.0 (May 2021)
- search until 100% match is found and exit
- other misc changes
v0.1.2 (April 2021)
For the changelog of earlier versions, check the git commit history.