MagicHaskeller

This library implicitly re-exports the entities from module Language.Haskell.TH as TH and module Data.Typeable from the Standard Hierarchical Library of Haskell. Please refer to their documentations on types from them --- in this documentation, types from TH are all qualified and the only type used from module Typeable is Typeable.Typeable. Other types you had never seen should be our internal representation.

Setting up your synthesis

Before synthesis, you have to define at least one program generator algorithm (or you may define one once and reuse it for later syntheses). Other parameters are memoization depth and time out interval, which have default values. You may elect either to set those values to the 'global variables' using 'set*' functions (i.e. functions whose names are prefixed by set), or hand them explicitly as parameters.

Class for program generator algorithms

Please note that ConstrL and ConstrLSF are obsoleted and users are expected to use the constrL option in Option.

class ProgramGenerator a

ProgramGenerator is a generalization of the old Memo type.

Instances

ProgramGenerator ProgGen
Expression e => ProgramGenerator (PGSF e)

data ProgGen

The vanilla program generator corresponding to Version 0.7.*

Instances

ProgramGenerator ProgGen

type ProgGenSF = PGSF AnnExpr

Functions for creating your program generator algorithm

You can set your primitives like, e.g., setPrimitives $(p [| ( (+) :: Int->Int->Int, 0 :: Int, 'A', [] :: [a] ) |]), where the primitive set is consisted of (+) specialized to type Int->Int->Int, 0 specialized to type Int, 'A' which has monomorphic type Char, and [] with polymorphic type [a]. As primitive components one can include any variables and constructors within the scope. However, because currently ad hoc polymorphism is not supported by this library, you may not write setPrimitives $(p [| (+) :: Num a => a->a->a |]). Also, you have to specify the type unless you are using a primitive component whose type is monomorphic and instance of Data.Typeable.Typeable (just like when using the dynamic expression of Concurrent Clean), and thus you may write setPrimitives $(p [| 'A' |]), while you have to write setPrimitives $(p [| [] :: [a] |]) instead of setPrimitives $(p [| [] |]).

:: ExpQ	Quote a tuple of primitive components here.
-> ExpQ	This becomes `[Primitive]` when spliced.
`p` is used to convert your primitive component set into the internal form.

setPrimitives :: [Primitive] -> IO ()

setPrimitives creates a ProgGen from the given set of primitives using the current set of options, and sets it as the current program generator. It used to be equivalent to setPG . mkPG which overwrites the options with the default, but it is not now.

mkPG :: ProgramGenerator pg => [Primitive] -> pg

mkPG is defined as:

 mkPG prims = mkPGSF (mkStdGen 123456) (repeat 5) prims prims

mkPGSF

:: ProgramGenerator pg
=> StdGen
-> [Int]	number of random samples at each depth, for each type.
-> [Primitive]
-> [Primitive]
-> pg

setPG :: ProgGen -> IO ()

Older versions prohibited data types holding functions such as [a->b], (Int->Char, Bool), etc. just for efficiency reasons. They are still available if you use mkMemo and mkMemoSF instead of mkPG and mkPGSF respectively, though actually this limitation does not affect the efficiency a lot. (NB: recently I noticed that use of mkMemo or mkMemoSF might not improve the efficiency of generating lambda terms at all, though when I generated combinatory expressions it WAS necessary. In fact, I mistakenly turned this limitation off, and mkMemo and mkMemoSF were equivalent to mkPG and mkPGSF, but I did not notice that....)

mkMemo :: ProgramGenerator pg => [Primitive] -> pg

mkMemoSF

:: ProgramGenerator pg
=> StdGen
-> [Int]	number of random samples at each depth, for each type.
-> [Primitive]
-> [Primitive]
-> pg
`mkPGSF` and `mkMemoSF` are provided mainly for backward compatibility. These functions are defined only for the `ProgramGenerator`s whose names end with `SF` (i.e., generators with synergetic filtration). For such generators, they are defined as: mkPGSF gen nrnds optups tups = mkPGOpt (options{primopt = Just optups, contain = True, stdgen = gen, nrands = nrnds}) tups mkMemoSF gen nrnds optups tups = mkPGOpt (options{primopt = Just optups, contain = False, stdgen = gen, nrands = nrnds}) tups

mkMemo075 enables some more old good optimization options used until Version 0.7.5, including guess on the primitive functions. It is for you if you prefer speed, but the result can be non-exhaustive if you use it with your own LibTH.hs. Also, you need to use the prefixed |(->)| in order for the options to take effect. See LibTH.hs for examples.

mkPG075 :: ProgramGenerator pg => [Primitive] -> pg

mkMemo075 :: ProgramGenerator pg => [Primitive] -> pg

mkPGOpt can be used along with its friends instead of mkPG when the search should be fine-tuned.

mkPGOpt :: ProgramGenerator pg => Options -> [Primitive] -> pg

type Options = Opt [Primitive]

options for limiting the hypothesis space.

data Opt a

options that limit the hypothesis space.

Constructors

Opt

primopt :: Maybe a	Use this option if you want to use a different component library for the stage of solving the inhabitation problem. `Nothing` means using the same one. This option makes sense only when using *SF style generators, because otherwise the program generation is not staged. Using a minimal set for solving the inhabitation and a redundant library for the real program generation can be a good bet.
memodepth :: Int	memoization depth. (Sub)expressions within this size are memoized, while greater expressions will be recomputed (to save the heap space). Only effective when using ProgGen and unless using the everythingIO family.
memoCond :: MemoCond	This represents which memoization table to be used based on the query type and the search depth, when using the everythingIO family.
execute :: VarLib -> CoreExpr -> Dynamic
timeout :: Maybe Int	`Just ms` sets the timeout to `ms` microseconds. Also, my implementation of timeout also catches inevitable exceptions like stack space overflow. Note that setting timeout makes the library referentially untransparent. (But currently `Just 20000` is the default!) Setting this option to `Nothing` disables both timeout and capturing exceptions.
forcibleTimeout :: Bool	If this option is `True`, System.Posix.Process.forkProcess instead of Control.Concurrent.forkIO is used for timeout. The former is much heavier than the latter, but is more preemptive and thus is necessary for interrupting some infinite loops. This record is ignored if FORCIBLETO is not defined.
guess :: Bool	If this option is `True`, the program guesses whether each function is a casecatamorphismparamorphism or not. This information is used to filter out some duplicate expressions. (History: I once abandoned this guessing strategy around the time I moved to the library implementation, because I could not formally prove the exhaustiveness of the resulting algorithm. For this reason, the old standalone version of MagicHaskeller uses this strategy, but almost the same effect can be obtained by setting this option to True, or using MagicHaskeller.init075 instead of MagicHaskeller.initialize.
contain :: Bool	This option is now obsolete, and we always assume True now. If this option was `False`, data structures might not contain functions, and thus types like `[Int->Int]`, `(Int->Bool, Char)`, etc. were not permitted. (NB: recently I noticed that making this `False` might not improve the efficiency of generating lambda terms at all, though when I generated combinatory expressions it WAS necessary. In fact, I mistakenly turned this limitation off, and my code always regarded this as True, but I did not notice that, so this option can be obsoleted.)
constrL :: Bool	If this option is `True`, matching at the antecedent of induction rules may occur, which constrains generation of existential types. You need to use prefixed `(->)` to show that some parameter can be matched at the antecedent, e.g., `p [\| ( []::[a], (:)::a->[a]->[a], foldr :: (a->b->b) -> b -> (->) [a] b ) \|]` See LibTH.hs for examples.
tvndelay :: Int	Each time the type variable which appears in the return type of a function (e.g. `b` in `foldr::(a->b->b)->b->[a]->b`) is expanded to a function type, the search priority of the current computation is lowered by this number. It's default value is 1, which means there is nothing special, and the priority for each expression corresponds to the number of function applications in the expression. Example: when tvndelay = 1, The priority of \xs -> foldr (\x y -> x+y) 0 xs is 5, because there are five `$`'s in \xs -> ((foldr $ (\x y -> ((+) $ x) $ y)) $ 0) xs The priority of \xs ys -> foldr (\x y zs -> x : y zs) (\ws->ws) xs ys is 7, because there are seven `$`'s in \xs ys -> (((foldr $ (\x y zs -> (((:) $ x) $ y) $ zs)) $ (\ws->ws)) $ xs) $ ys Example: when tvndelay = 2, The priority of \xs -> foldr (\x y -> x+y) 0 xs is 5, because there are five `$`'s in \xs -> ((foldr $ (\x y -> ((+) $ x) $ y)) $ 0) xs The priority of \xs ys -> foldr (\x y zs -> x : y zs) (\ws->ws) xs ys is 8, because there are eight `$`'s in \xs ys -> (((foldr $ (\x y zs -> (((:) $ x) $ y) $ zs)) $ (\ws->ws)) $ xs) $$ ys where `$$` denotes the function application caused by expanding a type variable into a function type.
tv1 :: Bool	If this option is `True`, the return type of functions returning a type variable (e.g. `b` in `foldr::(a->b->b)->b->[a]->b`) can only be replaced with `Eval t => t` and `Eval t => u -> t`, while if `False` with `Eval t => t`, `Eval t => u->t`, `Eval t => u->v->t`, etc., where `Eval t` means t cannot be replaced with a function. The restriction can be amended if the tuple constructor and destructors are available.
tv0 :: Bool
stdgen :: StdGen	The random seed.
nrands :: [Int]	number of random samples at each depth, for each type.

options :: Opt a

default options

 options = Opt{ primopt = Nothing
              , memodepth = 10
              , memoCond = \ _type depth -> return $ if depth < 10 then Ram else Recompute
              , execute = unsafeExecute
              , timeout = Just 20000
              , forcibleTimeout = False
              , guess   = False
              , contain = True
              , constrL = False
              , tv1     = False
              , stdgen  = mkStdGen 123456
              , nrands  = repeat 5
              }

data MemoType

Constructors

Recompute	Recompute instead of memoizing.
Ram	Use the memoization table based on lazy evaluation, like in older versions.
Disk FilePath	Use the directory specified by `FilePath` as the persistent memoization table.

Memoization depth

NB: setDepth will be obsoleted. It is provided for backward compatibility, but not exactly compatible with the old one in that its result will not affect the behavior of everything, etc., which explicitly take a ProgramGenerator as an argument. Also, in the current implementation, the result of setDepth will be overwritten by setPrimitives. Use memodepth option instead.

setDepth

:: Int	memoization depth. (Sub)expressions within this size are memoized, while greater expressions will be recomputed (to save the heap space).
-> IO ()
Currently the default depth is 10. You may want to lower the value if your computer often swaps, or increase it if you have a lot of memory.

Time out

NB: setTimeout and unsetTimeout will be obsoleted. They are provided for backward compatibility, but not exactly compatible with the old ones in that their results will not affect the behavior of everything, etc., which explicitly take a ProgramGenerator as an argument. Also, in the current implementation, the result of setTimeout and unsetTimeout will be overwritten by setPrimitives. Use timeout option instead.

Because the library generates all the expressions including those with non-linear recursions, you should note that there exist some expressions which take extraordinarily long time. (Imagine a function that takes an integer n and increments 0 for 2^(2^n) times.) For this reason, time out is taken after 0.02 second since each invocation of evaluation by default. This default behavior can be overridden by the following functions.

setTimeout

:: Int	time in microseconds
-> IO ()
`setTimeout` sets the timeout in microseconds. Also, my implementation of timeout also catches inevitable exceptions like stack space overflow. Note that setting timeout makes the library referentially untransparent. (But currently `setTimeout 20000` is the default!)

unsetTimeout :: IO ()

unsetTimeout disables timeout. This is the safe choice.

Defining functions automatically

In this case "automatically" does not mean "inductively" but "deductively using Template Haskell";)

define :: Name -> String -> ExpQ -> Q [Dec]

define eases use of this library by automating some function definitions. For example,

 $( define ''ProgGen "Foo" (p [| (1 :: Int, (+) :: Int -> Int -> Int) |]) )

is equivalent to

 memoFoo :: ProgGen
 memoFoo = mkPG (p [| (1 :: Int, (+) :: Int -> Int -> Int) |])
 everyFoo :: Everything
 everyFoo = everything memoFoo
 filterFoo :: Filter
 filterFoo pred = filterThen pred everyFoo

If you do not think this function reduces the number of your keystrokes a lot, you can do without it.

type Everything = Typeable a => Every a

type Filter = Typeable a => (a -> Bool) -> IO (Every a)

type Every a = [[(Exp, a)]]

type EveryIO a = Int -> IO [(Exp, a)]

Generating programs

(There are many variants, but most of the functions here just filter everything with the predicates you provide.)

Functions suffixed with "F" (like everythingF, etc.) are filtered versions, where their results are filtered to totally remove semantic duplications. In general they are equivalent to applying everyF afterwards. (Note that this is filtration AFTER the program generation, unlike the filtration by using ProgGenSF is done DURING program generation.)

Quick start

findOne :: Typeable a => (a -> Bool) -> Exp

findOne pred finds an expression e that satisfies pred e == True, and returns it in Exp.

printOne :: Typeable a => (a -> Bool) -> IO Exp

printOne prints the expression found first.

printAll :: Typeable a => (a -> Bool) -> IO ()

printAllF :: (Typeable a, Filtrable a) => (a -> Bool) -> IO ()

io2pred :: Eq b => [(a, b)] -> (a -> b) -> Bool

io2pred converts a specification given as a set of I/O pairs to the predicate form which other functions accept.

Incremental filtration

Sometimes you may want to filter further after synthesis, because the predicate you previously provided did not specify the function enough. The following functions can be used to filter expressions incrementally.

filterFirst :: Typeable a => (a -> Bool) -> IO (Every a)

filterFirst is like printAll, but by itself it does not print anything. Instead, it creates a stream of expressions represented in tuples of Exp and the expressions themselves.

filterFirstF :: (Typeable a, Filtrable a) => (a -> Bool) -> IO (Every a)

filterThen :: Typeable a => (a -> Bool) -> Every a -> IO (Every a)

filterThen may be used to further filter the results.

filterThenF :: (Typeable a, Filtrable a) => (a -> Bool) -> Every a -> IO (Every a)

Expression generators

These functions generate all the expressions that have the type you provide.

getEverything :: Typeable a => IO (Every a)

getEverything uses the 'global' values set with set* functions. getEverythingF is its filtered version

everything

:: (ProgramGenerator pg, Typeable a)
=> pg	program generator
-> Every a

everythingM

:: (ProgramGenerator pg, Typeable a, Monad m, Functor m)
=> pg	program generator
-> Int	query depth
-> m [(Exp, a)]

everythingIO

:: (ProgramGenerator pg, Typeable a)
=> pg	program generator
-> EveryIO a

unifyable

:: ProgramGenerator pg
=> pg	program generator
-> Type	query type
-> [[Exp]]
Those functions are like `everything`, but take `Type` as an argument, which may be polymorphic. For example, `printQ ([t\| forall a. a->a->a \|] >>= return . unifyable True 10 memo)` will print all the expressions using `memo` whose types unify with `forall a. a->a->a`. (At first I (Susumu) could not find usefulness in finding unifyable expressions, but seemingly Hoogle does something alike, and these functions might enhance it.)

matching

:: ProgramGenerator pg
=> pg	program generator
-> Type	query type
-> [[Exp]]

getEverythingF :: Typeable a => IO (Every a)

everythingF

:: (ProgramGenerator pg, Typeable a)
=> pg	program generator
-> Every a
`everything` generates all the expressions that fit the inferred type, and their representations in the `Exp` form. It returns a stream of lists, which is equivalent to Spivey's `Matrix` data type, i.e., that contains expressions consisted of n primitive components at the n-th element (n = 1,2,...). `everythingF` is its filtered version

unifyableF

:: ProgramGenerator pg
=> pg	program generator
-> Type	query type
-> [[Exp]]

matchingF

:: ProgramGenerator pg
=> pg	program generator
-> Type	query type
-> [[Exp]]

Utility to filter out equivalent expressions

everyF

:: (Typeable a, Filtrable a)
=> Maybe Int	microsecs until timeout
-> Every a
-> Every a

Unility to get one value easily

stripEvery :: Every a -> a

Pretty printers

pprs :: Every a -> IO ()

pprs pretty prints the results to the console, using pprintUC

pprsIO :: EveryIO a -> IO ()

pprsIO is the EveryIO version of pprs

pprsIOn :: Int -> EveryIO a -> IO ()

pprsIOn depth eio is the counterpart of pprs (take depth eio), while pprsIO eio is the counterpart of pprs eio. Example: pprsIOn 5 (everythingIO (mlist::ProgGen) :: EveryIO ([Char]->[Char]))

lengths :: Every a -> IO ()

lengthsIO :: EveryIO a -> IO ()

lengthsIOn :: Int -> EveryIO a -> IO ()

printQ :: (Ppr a, Data a) => Q a -> IO ()

Internal data representation

The following types are assigned to our internal data representations.

type Primitive = (HValue, Exp, Type)

newtype HValue

Constructors

HV (forall a. a)

unsafeCoerce# :: a -> b

The function unsafeCoerce# allows you to side-step the typechecker entirely. That is, it allows you to coerce any type into any other type. If you use this function, you had better get it right, otherwise segmentation faults await. It is generally used when you want to write a program that you know is well-typed, but where Haskell's type system is not expressive enough to prove that it is well typed.

The following uses of unsafeCoerce# are supposed to work (i.e. not lead to spurious compile-time or run-time crashes):

Casting any lifted type to Any
Casting Any back to the real type
Casting an unboxed type to another unboxed type of the same size (but not coercions between floating-point and integral types)
Casting between two types that have the same runtime representation. One case is when the two types differ only in "phantom" type parameters, for example Ptr Int to Ptr Float, or [Int] to [Float] when the list is known to be empty. Also, a newtype of a type T has the same representation at runtime as T.

Other uses of unsafeCoerce# are undefined. In particular, you should not use unsafeCoerce# to cast a T to an algebraic data type D, unless T is also an algebraic data type. For example, do not cast Int->Int to Bool, even if you later cast that Bool back to Int->Int before applying it. The reasons have to do with GHC's internal representation details (for the congnoscenti, data values can be entered but function closures cannot). If you want a safe type to cast things to, use Any, which is not an algebraic data type.

exprToTHExp :: VarLib -> CoreExpr -> Exp

trToTHType :: TypeRep -> Type

printAny :: Typeable a => (a -> Bool) -> IO ()

printAll prints all the expressions satisfying the given predicate.

p1 :: Exp -> ExpQ

class Filtrable a

Instances

Ord a => Filtrable a
(RealFloat a, Ord a) => Filtrable (Complex a)
(Arbitrary a, Filtrable r) => Filtrable (a -> r)

Produced by Haddock version 2.7.2