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:

factorial :: Int -> Int
factorial 2  =  2
factorial 3  =  6
factorial 4  =  24

ingredients :: [Ingredient]
ingredients  =
  [ con (0::Int)
  , con (1::Int)
  , fun "+" ((+) :: Int -> Int -> Int)
  , fun "*" ((*) :: Int -> Int -> Int)
  , fun "-" ((-) :: Int -> Int -> Int)
  ]

The conjure function does the following:

> conjure "factorial" factorial ingredients
factorial :: Int -> Int
-- 0.1s, testing 4 combinations of argument values
-- 0.8s, pruning with 27/65 rules
-- ...  ...  ...  ...  ...  ...
-- 0.9s, 35 candidates of size 6
-- 0.9s, 167 candidates of size 7
-- 0.9s, tested 95 candidates
factorial 0  =  1
factorial x  =  x * factorial (x - 1)

The ingredients list is defined with con and fun.

A single functional ingredient in conjuring. Specify conjure ingredients with con and fun:

conjure "foo" foo [ con False
                  , con True
                  , con (0 :: Int)
                  , con (1 :: Int)
                  , ...
                  , fun "&&" (&&)
                  , fun "||" (||)
                  , fun "+" ((+) :: Int -> Int -> Int)
                  , fun "*" ((*) :: Int -> Int -> Int)
                  , fun "-" ((-) :: Int -> Int -> Int)
                  , ...
                  ]

Ingredients may include arbitrary constants (con), constructors (con) or functions (fun). These may be built-in or user defined. Use con on Show instances and fun otherwise.

This is internally an arbitrary atomic Expression paired with a Reification of type information.

Provides a constant or constructor as an ingredient to Conjure. To be used on Show instances. (cf. fun)

conjure "foo" foo [ con False
                  , con True
                  , con (0 :: Int)
                  , con (1 :: Int)
                  , ...
                  ]

Argument types have to be monomorphized, so use type bindings when applicable.

Provided a Show-able non-functional value to Conjure. (cf. fun)

conjure "foo" foo [ unfun False
                  , unfun True
                  , unfun (0 :: Int)
                  , unfun (1 :: Int)
                  , ...
                  ]

Argument types have to be monomorphized, so use type bindings when applicable.

TODO: Make unfun the standard way to create encode Show values.

This is a replacement to con. In hindsight, con is not such a great name: constructors may be functional after all!

Provides a functional value as an ingredient to Conjure. To be used on values that are not Show instances such as functions. (cf. unfun, con)

conjure "foo" foo [ ...
                  , fun "&&" (&&)
                  , fun "||" (||)
                  , fun "+" ((+) :: Int -> Int -> Int)
                  , fun "*" ((*) :: Int -> Int -> Int)
                  , fun "-" ((-) :: Int -> Int -> Int)
                  , ...
                  ]

Argument types have to be monomorphized, so use type bindings when applicable.

Provides a guard bound to the conjured function's return type.

Guards are only alllowed at the root fo the RHS.

last' :: [Int] -> Int
last' [x]  =  x
last' [x,y]  =  y
last' [x,y,z]  =  z

> conjure "last" last'
>   [ con ([] :: [Int])
>   , fun ":" ((:) :: Int -> [Int] -> [Int])
>   , fun "null" (null :: [Int] -> Bool)
>   , guard
>   , fun "undefined" (undefined :: Int)
>   ]
last :: [Int] -> Int
-- 0.0s, testing 360 combinations of argument values
-- 0.0s, pruning with 5/5 rules
-- 0.0s, 1 candidates of size 1
-- 0.0s, 0 candidates of size 2
-- 0.0s, 0 candidates of size 3
-- 0.0s, 0 candidates of size 4
-- 0.0s, 0 candidates of size 5
-- 0.0s, 0 candidates of size 6
-- 0.0s, 4 candidates of size 7
-- 0.0s, tested 2 candidates
last []  =  undefined
last (x:xs)
  | null xs  =  x
  | otherwise  =  last xs

Provides an if condition bound to the given return type as a Conjure ingredient.

This should be used when one wants Conjure to consider if-expressions at all:

last' :: [Int] -> Int
last' [x]  =  x
last' [x,y]  =  y
last' [x,y,z]  =  z

> conjure "last" last' [ con ([] :: [Int])
>                      , fun ":" ((:) :: Int -> [Int] -> [Int])
>                      , fun "null" (null :: [Int] -> Bool)
>                      , iif (undefined :: Int)
>                      , fun "undefined" (undefined :: Int)
>                      ]
last :: [Int] -> Int
-- 0.0s, testing 360 combinations of argument values
-- 0.0s, pruning with 5/5 rules
-- ...   ...   ...   ...   ...
-- 0.0s, 4 candidates of size 7
-- 0.0s, tested 2 candidates
last []  =  undefined
last (x:xs)  =  if null xs
                then x
                else last xs

Provides a case condition bound to the given return type.

This should be used when one wants Conjure to consider ord-case expressions:

> conjure "mem" mem
>   [ con False
>   , con True
>   , fun "`compare`" (compare :: Int -> Int -> Ordering)
>   , ordcase (undefined :: Bool)
>   ]
mem :: Int -> Tree -> Bool
-- ...   ...   ...   ...   ...
-- 0.0s, 384 candidates of size 12
-- 0.0s, tested 346 candidates
mem x Leaf  =  False
mem x (Node t1 y t2)  =  case x `compare` y of
                         LT -> mem x t1
                         EQ -> True
                         GT -> mem x t2

By default, conjure tests candidates up to a maximum of 360 tests. This configures the maximum number of tests to each candidate, when provided in the list of ingredients:

conjure "..." ... [ ...
                  , maxTests 1080
                  , ... ]

By default, conjure targets testing 10080 candidates. This configures a different target when provided in the list of ingredients:

conjure "..." ... [ ...
                  , target 5040
                  , ... ]

By default, conjure imposes no limit on the size of candidates.

This configures a different maximum when provided in the list of ingredients.

If only one of maxSize and target is defined, it is used. If none, target is used.

Conjures an implementation from a function specification.

This function works like conjure but instead of receiving a partial definition it receives a boolean filter / property about the function.

For example, given:

squareSpec :: (Int -> Int) -> Bool
squareSpec square  =  square 0 == 0
                   && square 1 == 1
                   && square 2 == 4

Then:

> conjureFromSpec "square" squareSpec [fun "*" ((*) :: Int -> Int -> Int)]
square :: Int -> Int
-- 0.1s, pruning with 2/6 rules
-- 0.1s, 1 candidates of size 1
-- 0.1s, 0 candidates of size 2
-- 0.1s, 1 candidates of size 3
-- 0.1s, tested 2 candidates
square x  =  x * x

This allows users to specify QuickCheck-style properties, here is an example using LeanCheck:

import Test.LeanCheck (holds, exists)

squarePropertySpec :: (Int -> Int) -> Bool
squarePropertySpec square  =  and
  [ holds n $ \x -> square x >= x
  , holds n $ \x -> square x >= 0
  , exists n $ \x -> square x > x
  ]  where  n = 60

Class of Conjurable types. Functions are Conjurable if all their arguments are Conjurable, Listable and Showable.

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.

Conjurable instances can be derived automatically using deriveConjurable.

(cf. reifyTiers, reifyEquality, conjureType)

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.

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

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]

Reifies the expr function in a Conjurable type instance.

This is to be used in the definition of conjureExpress of Conjurable typeclass instances.

instance ... => Conjurable <Type> where
  ...
  conjureExpress  =  reifyExpress
  ...

Reifies equality == in a Conjurable type instance.

This is to be used in the definition of conjureEquality of Conjurable typeclass instances:

instance ... => Conjurable <Type> where
  ...
  conjureEquality  =  reifyEquality
  ...

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
  ...

To be used in the implementation of conjureSubTypes.

instance ... => Conjurable <Type> where
  ...
  conjureSubTypes x  =  conjureType (field1 x)
                     .  conjureType (field2 x)
                     .  ...
                     .  conjureType (fieldN x)
  ...

If we were to come up with a variable name for the given type what name would it be?

An instance for a given type Ty is simply given by:

instance Name Ty where name _ = "x"

Examples:

> name (undefined :: Int)
"x"

> name (undefined :: Bool)
"p"

> name (undefined :: [Int])
"xs"

This is then used to generate an infinite list of variable names:

> names (undefined :: Int)
["x", "y", "z", "x'", "y'", "z'", "x''", "y''", "z''", ...]

> names (undefined :: Bool)
["p", "q", "r", "p'", "q'", "r'", "p''", "q''", "r''", ...]

> names (undefined :: [Int])
["xs", "ys", "zs", "xs'", "ys'", "zs'", "xs''", "ys''", ...]

Express typeclass instances provide an expr function that allows values to be deeply encoded as applications of Exprs.

expr False  =  val False
expr (Just True)  =  value "Just" (Just :: Bool -> Maybe Bool) :$ val True

The function expr can be contrasted with the function val:

• val always encodes values as atomic Value Exprs -- shallow encoding.
• expr ideally encodes expressions as applications (:$) between Value Exprs -- deep encoding.

Depending on the situation, one or the other may be desirable.

Instances can be automatically derived using the TH function deriveExpress.

The following example shows a datatype and its instance:

data Stack a = Stack a (Stack a) | Empty

instance Express a => Express (Stack a) where
  expr s@(Stack x y) = value "Stack" (Stack ->>: s) :$ expr x :$ expr y
  expr s@Empty       = value "Empty" (Empty   -: s)

To declare expr it may be useful to use auxiliary type binding operators: -:, ->:, ->>:, ->>>:, ->>>>:, ->>>>>:, ...

For types with atomic values, just declare expr = val

Derives an Conjurable instance for the given type Name.

If not already present, this also derives Listable, Express and Name instances.

If the Data.Express' type binding operators (-:, ->: or ->>:) are not in scope, this derives them as well.

This function needs the TemplateHaskell extension. You can place the following at the top of the file:

{-# LANGUAGE TemplateHaskell #-}
import Conjure
import Test.LeanCheck

Then just call deriveConjurable after your data type declaration:

data Peano  =  Z | S Peano  deriving  (Show, Eq)

deriveConjurable ''Peano

deriveConjurable expects the argument type to be an instance of Show and Eq.

Same as deriveConjurable but does not warn when instance already exists (deriveConjurable is preferable).

Derives a Conjurable instance for a given type Name cascading derivation of type arguments as well.

Results to the conjpure family of functions. This is for advanced users. One is probably better-off using the conjure family.

Like conjure but in the pure world.

The most important part of the result are the tiers of implementations however results also include candidates, tests and the underlying theory.

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

This type is homomorphic to A, Nat6, C, D, E and F.

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]

This type is homomorphic to A, B, Nat6, D, E and F.