code-conjure: synthesize Haskell functions out of partial definitions

[ bsd3, haskell, library ] [ Propose Tags ]

Conjure is a tool that synthesizes Haskell functions out of partial definitions.


[Skip to Readme]
Versions [RSS] [faq] 0.0.2, 0.0.4, 0.1.0, 0.1.2, 0.2.0, 0.2.2, 0.2.4, 0.2.6, 0.2.8, 0.3.0, 0.3.2, 0.3.4, 0.3.6, 0.4.0, 0.4.2, 0.4.4, 0.5.0
Change log changelog.md
Dependencies base (==4.*), express (>=1.0.8), leancheck (>=0.9.10), speculate (>=0.4.14), template-haskell [details]
License BSD-3-Clause
Author Rudy Matela
Maintainer Rudy Matela <rudy@matela.com.br>
Category Haskell
Home page https://github.com/rudymatela/conjure#readme
Source repo head: git clone https://github.com/rudymatela/conjure
this: git clone https://github.com/rudymatela/conjure(tag v0.5.0)
Uploaded by rudymatela at 2021-09-20T22:33:39Z
Distributions NixOS:0.4.4
Downloads 2103 total (416 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2021-09-20 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees

Candidates


Readme for code-conjure-0.5.0

[back to package description]

Conjure

Conjure's Build Status Conjure on Hackage Conjure on Stackage LTS Conjure on Stackage Nightly

Conjure logo

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 v1-install code-conjure

If you are using Cabal v3.0 or later, avoid using cabal install for the time being and use v1-install instead.

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.

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:

  1. Conjure may fail to "hit" the appropriate data points;
  2. 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.

MagicHaskeller (2007) is another tool that is able to generate Haskell code automatically. It supports recursion through catamorphisms, paramorphisms and the fix function.

Barliman for Lisp is another tool that does program synthesis.

There are hundreds of others, I'll add the most closely related here when I have the time.

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 Rudy Matela, distribued under the 3-clause BSD license.