Copyright | (c) 2021 Rudy Matela |
---|---|
License | 3-Clause BSD (see the file LICENSE) |
Maintainer | Rudy Matela <rudy@matela.com.br> |
Safe Haskell | None |
Language | Haskell2010 |
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:
primitives :: [Expr] primitives = [ val (0::Int) , val (1::Int) , value "+" ((+) :: Int -> Int -> Int) , value "*" ((*) :: Int -> Int -> Int) ]
Step 3: call conjure and see your generated function:
> conjure "square" square primitives square :: Int -> Int -- testing 3 combinations of argument values -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 5 candidates of size 3 square x = x * x
Synopsis
- conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
- val :: (Typeable a, Show a) => a -> Expr
- value :: Typeable a => String -> a -> Expr
- data Expr
- conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()
- conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
- data Args = Args {
- maxTests :: Int
- maxSize :: Int
- maxRecursiveCalls :: Int
- maxEquationSize :: Int
- maxRecursionSize :: Int
- maxSearchTests :: Int
- forceTests :: [[Expr]]
- args :: Args
- type Spec1 a b = [(a, b)]
- type Spec2 a b c = [((a, b), c)]
- type Spec3 a b c d = [((a, b, c), d)]
- (-=) :: a -> b -> (a, b)
- conjure1 :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Expr] -> IO ()
- conjure2 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => String -> Spec2 a b c -> [Expr] -> IO ()
- conjure3 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => String -> Spec3 a b c d -> [Expr] -> IO ()
- conjure1With :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Expr] -> IO ()
- conjure2With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()
- conjure3With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()
- class Typeable a => Conjurable a where
- conjureEquality :: a -> Maybe Expr
- conjureTiers :: a -> Maybe [[Expr]]
- reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr
- reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]]
- conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
- conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
- data A
- data B
- data C
- data D
- data E
- data F
Basic use
conjure :: Conjurable f => String -> f -> [Expr] -> IO () Source #
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 Expr
s.
For example, given:
square :: Int -> Int square 0 = 0 square 1 = 1 square 2 = 4 primitives :: [Expr] primitives = [ val (0::Int) , val (1::Int) , value "+" ((+) :: Int -> Int -> Int) , value "*" ((*) :: Int -> Int -> Int) ]
The conjure function does the following:
> conjure "square" square primitives square :: Int -> Int -- testing 3 combinations of argument values -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 5 candidates of size 3 square x = x * x
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]
Values of type Expr
represent objects or applications between objects.
Each object is encapsulated together with its type and string representation.
Values encoded in Expr
s are always monomorphic.
An Expr
can be constructed using:
val
, for values that areShow
instances;value
, for values that are notShow
instances, like functions;:$
, for applications betweenExpr
s.
> 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'
Show
ing 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 Expr
s usually follow the convention
where a value
whose String
representation starts with '_'
represents a var
iable.
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. |
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 ( |
Show Expr | Shows > show (value "not" not :$ val False) "not False :: Bool" |
Advanced use
conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO () Source #
Like conjure
but allows setting the maximum size of considered expressions
instead of the default value of 12.
conjureWithMaxSize 10 "function" function [...]
conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () Source #
Arguments to be passed to conjureWith
or conjpureWith
.
See args
for the defaults.
Args | |
|
Default arguments to conjure.
- 60 tests
- functions of up to 12 symbols
- maximum of 1 recursive call
- pruning with equations up to size 5
- recursion up to 60 symbols
- search for defined applications for up to 100000 combinations
Conjuring from a specification
type Spec1 a b = [(a, b)] Source #
A partial specification of a function with one argument:
sumSpec :: Spec1 [Int] Int sumSpec = [ [] -= 0 , [1,2] -= 3 , [3,4,5] -= 12 ]
To be passed as one of the arguments to conjure1
.
type Spec2 a b c = [((a, b), c)] Source #
A partial specification of a function with two arguments:
appSpec :: Spec2 [Int] [Int] [Int] appSpec = [ (,) [] [0,1] -= [0,1] , (,) [2,3] [] -= [2,3] , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9] ]
To be passed as one of the arguments to conjure2
.
type Spec3 a b c d = [((a, b, c), d)] Source #
A partial specification of a function with three arguments.
To be passed as one of the arguments to conjure3
conjure1 :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Expr] -> IO () Source #
Conjures a one argument function from a specification.
Given:
sumSpec :: Spec1 [Int] Int sumSpec = [ [] -= 0 , [1,2] -= 3 , [3,4,5] -= 12 ]
sumPrimitives :: [Expr] sumPrimitives = [ value "null" (null :: [Int] -> Bool) , val (0::Int) , value "+" ((+) :: Int -> Int -> Int) , value "head" (head :: [Int] -> Int) , value "tail" (tail :: [Int] -> [Int]) ]
Then:
> conjure1 "sum" sumSpec sumPrimitives sum :: [Int] -> Int -- testing 3 combinations of argument values -- ... -- looking through 189/465 candidates of size 10 xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)
(cf. Spec1
, conjure1With
)
conjure2 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => String -> Spec2 a b c -> [Expr] -> IO () Source #
Conjures a two argument function from a specification.
Given:
appSpec :: Spec2 [Int] [Int] [Int] appSpec = [ (,) [] [0,1] -= [0,1] , (,) [2,3] [] -= [2,3] , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9] ]
appPrimitives :: [Expr] appPrimitives = [ value "null" (null :: [Int] -> Bool) , value ":" ((:) :: Int -> [Int] -> [Int]) , value "head" (head :: [Int] -> Int) , value "tail" (tail :: [Int] -> [Int]) ]
Then:
> conjure2 "++" appSpec appPrimitives (++) :: [Int] -> [Int] -> [Int] -- testing 3 combinations of argument values -- ... -- looking through 26166/57090 candidates of size 11 xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)
(cf. Spec2
, conjure2With
)
conjure3 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => String -> Spec3 a b c d -> [Expr] -> IO () Source #
Conjures a three argument function from a specification.
(cf. Spec3
, conjure3With
)
conjure1With :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Expr] -> IO () Source #
conjure2With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c) => Args -> String -> Spec2 a b c -> [Expr] -> IO () Source #
conjure3With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d, Eq d) => Args -> String -> Spec3 a b c d -> [Expr] -> IO () Source #
When using custom types
class Typeable a => Conjurable a where Source #
Class of Conjurable
types.
Functions are Conjurable
if all their arguments are Conjurable
, Listable
and Show
able.
For atomic types that are Listable
,
instances are defined as:
instance Conjurable Atomic where conjureTiers = reifyTiers
For atomic types that are both Listable
and Eq
,
instances are defined as:
instance Conjurable Atomic where conjureTiers = reifyTiers conjureEquality = reifyEquality
For types with subtypes, instances are defined as:
instance Conjurable Composite where conjureTiers = reifyTiers conjureEquality = reifyEquality conjureSubTypes x = conjureType y . conjureType z . conjureType w where (Composite ... y ... z ... w ...) = x
Above x
, y
, z
and w
are just proxies.
The Proxy
type was avoided for backwards compatibility.
Please see the source code of Conjure.Conjurable for more examples.
(cf. reifyTiers
, reifyEquality
, conjureType
)
Nothing
conjureEquality :: a -> Maybe Expr Source #
conjureTiers :: a -> Maybe [[Expr]] Source #
Instances
reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr Source #
Reifies equality to be used in a conjurable type.
This is to be used
in the definition of conjureEquality
of Conjurable
typeclass instances:
instance ... => Conjurable <Type> where ... conjureEquality = reifyEquality ...
reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]] Source #
Reifies equality to be used in a conjurable type.
This is to be used
in the definition of conjureTiers
of Conjurable
typeclass instances:
instance ... => Conjurable <Type> where ... conjureTiers = reifyTiers ...
Pure interfaces
conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr]) Source #
Like conjure
but in the pure world.
Returns a triple with:
- tiers of implementations
- tiers of candidate bodies (right type)
- tiers of candidate expressions (any type)
- a list of tests
conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr]) Source #
Helper test types
Generic type A
.
Can be used to test polymorphic functions with a type variable
such as take
or sort
:
take :: Int -> [a] -> [a] sort :: Ord a => [a] -> [a]
by binding them to the following types:
take :: Int -> [A] -> [A] sort :: [A] -> [A]
This type is homomorphic to Nat6
, B
, C
, D
, E
and F
.
It is instance to several typeclasses so that it can be used to test functions with type contexts.
Generic type B
.
Can be used to test polymorphic functions with two type variables
such as map
or foldr
:
map :: (a -> b) -> [a] -> [b] foldr :: (a -> b -> b) -> b -> [a] -> b
by binding them to the following types:
map :: (A -> B) -> [A] -> [B] foldr :: (A -> B -> B) -> B -> [A] -> B
Generic type C
.
Can be used to test polymorphic functions with three type variables
such as uncurry
or zipWith
:
uncurry :: (a -> b -> c) -> (a, b) -> c zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
by binding them to the following types:
uncurry :: (A -> B -> C) -> (A, B) -> C zipWith :: (A -> B -> C) -> [A] -> [B] -> [C]
Generic type D
.
Can be used to test polymorphic functions with four type variables.
Generic type E
.
Can be used to test polymorphic functions with five type variables.