Conjure

A library for Conjuring function implementations from tests or partial definitions. (a.k.a.: functional inductive programming)

This is currently an experimental tool in its early stages, don't expect much from its current version. It is just a piece of curiosity in its current state.

Step 1: declare your partial function

square :: Int -> Int
square 0  =  0
square 1  =  1
square 2  =  4

Step 2: declare a list with the potential building blocks:

background :: [Expr]
background =
  [ val (0::Int)
  , val (1::Int)
  , value "+" ((+) :: Int -> Int -> Int)
  , value "*" ((*) :: Int -> Int -> Int)
  , value "==" ((==) :: Int -> Int -> Bool)
]

Including equality == over the given type is a good rule of thumb to improve performance.

Step 3: call conjure and see your generated function:

> conjure "square" square background
square :: Int -> Int
-- looking through 815 candidates, 100% match, 3/3 assignments
square x  =  x * x

Basic use

conjure :: Conjurable f => String -> f -> [Expr] -> IO ()

Conjures an implementation of a partially defined function.

Takes a String with the name of a function, a partially-defined function from a conjurable type, and a list of building blocks encoded as Exprs.

For example, given:

square :: Int -> Int
square 0  =  0
square 1  =  1
square 2  =  4

background :: [Expr]
background =
  [ val (0::Int)
  , val (1::Int)
  , value "+" ((+) :: Int -> Int -> Int)
  , value "*" ((*) :: Int -> Int -> Int)
  , value "==" ((==) :: Int -> Int -> Bool)
]

The conjure function does the following:

> conjure "square" square background
square :: Int -> Int
-- looking through 815 candidates, 100% match, 3/3 assignments
square x  =  x * x

The background is defined with val, value and ifFor.

val :: (Typeable a, Show a) => a -> Expr

O(1). A shorthand for value for values that are Show instances.

> val (0 :: Int)
0 :: Int

> val 'a'
'a' :: Char

> val True
True :: Bool

Example equivalences to value:

val 0     =  value "0" 0
val 'a'   =  value "'a'" 'a'
val True  =  value "True" True

value :: Typeable a => String -> a -> Expr

O(1). It takes a string representation of a value and a value, returning an Expr with that terminal value. For instances of Show, it is preferable to use val.

> value "0" (0 :: Integer)
0 :: Integer

> value "'a'" 'a'
'a' :: Char

> value "True" True
True :: Bool

> value "id" (id :: Int -> Int)
id :: Int -> Int

> value "(+)" ((+) :: Int -> Int -> Int)
(+) :: Int -> Int -> Int

> value "sort" (sort :: [Bool] -> [Bool])
sort :: [Bool] -> [Bool]

ifFor :: Typeable a => a -> Expr

Creates an if Expr of the type of the given proxy.

> ifFor (undefined :: Int)
if :: Bool -> Int -> Int -> Int

> ifFor (undefined :: String)
if :: Bool -> [Char] -> [Char] -> [Char]

You need to provide this as part of your building blocks on the background if you want recursive functions to be considered and produced.

data Expr

Values of type Expr represent objects or applications between objects. Each object is encapsulated together with its type and string representation. Values encoded in Exprs are always monomorphic.

An Expr can be constructed using:

• val, for values that are Show instances;
• value, for values that are not Show instances, like functions;
• :$, for applications between Exprs.

> val False
False :: Bool

> value "not" not :$ val False
not False :: Bool

An Expr can be evaluated using evaluate, eval or evl.

> evl $ val (1 :: Int) :: Int
1

> evaluate $ val (1 :: Int) :: Maybe Bool
Nothing

> eval 'a' (val 'b')
'b'

Showing a value of type Expr will return a pretty-printed representation of the expression together with its type.

> show (value "not" not :$ val False)
"not False :: Bool"

Expr is like Dynamic but has support for applications and variables (:$, var).

The var underscore convention: Functions that manipulate Exprs usually follow the convention where a value whose String representation starts with '_' represents a variable.

Instances

Eq Expr

O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types.

This instance works for ill-typed expressions.

Defined in Data.Express.Core

Methods

(==) :: Expr -> Expr -> Bool

(/=) :: Expr -> Expr -> Bool

Ord Expr

O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types.

This instance works for ill-typed expressions.

Expressions come first when they have smaller complexity (compareComplexity) or when they come first lexicographically (compareLexicographically).

Defined in Data.Express.Core

Methods

compare :: Expr -> Expr -> Ordering

(<) :: Expr -> Expr -> Bool

(<=) :: Expr -> Expr -> Bool

(>) :: Expr -> Expr -> Bool

(>=) :: Expr -> Expr -> Bool

max :: Expr -> Expr -> Expr

min :: Expr -> Expr -> Expr

Show Expr

Shows Exprs with their types.

> show (value "not" not :$ val False)
"not False :: Bool"

Defined in Data.Express.Core

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Advanced use

conjpure :: Conjurable f => String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])

Like conjure but in the pure world.

Returns a triple whose:

1. first element is the number of candidates considered
2. second element is the number of defined points in the given function
3. third element is a list of implementations encoded as Exprs paired with the number of matching points.

data Args

Arguments to be passed to conjureWith or conjpureWith. See args for the defaults.

Constructors

Args

Fields

• maxTests :: Int

  defaults to 60

• maxSize :: Int

  defaults to 9, keep greater than maxEquationSize

• maxEquationSize :: Int

  defaults to 5, keep smaller than maxSize

• maxRecursionSize :: Int

  defaults to 60

args :: Args

Default arguments to conjure.

• 60 tests
• functions of up to 9 symbols
• pruning with equations up to size 5
• recursion up to 60 symbols.

conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()

Like conjure but allows setting options through Args and args.

conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])

Like conjpure but allows setting options through Args and args.