On Sun, Jan 28, 2007 at 09:11:33PM +0100, Klaus Ostermann wrote:
I would like to have a program that can synthesize programs for a given type, composing only functions from a given library.
For example, suppose my library has
isZero :: Int -> Bool map :: (a -> b) -> [a] -> [b] and :: Bool -> Bool -> Bool fold :: (a -> b -> a) -> a -> [b] -> a True :: Bool (.) :: (b -> c) -> (a -> b) -> a -> c
Why just (.) ? I also assume your logic has modus ponens (curry howard: application)
then I want to ask, say, for a program of type
[Int] -> Bool
and get as answer
(fold and True) . (map isZero)
However, with none of these approaches I managed to do anything with list functions.
What else is available (besides Djinn and De-Typechecker)? Are lists a problem? In general, what are the practical and theoretical limits of these program synthesizers? Are there any overview papers for this topic?
A system (with the full axioms of intuitionist logic) would be much more likely to answer your query with \_ -> True . Not very helpful, eh? Lists are recursive types, and it is very easy for a list calculus to lose strong normalization. Without strong normalization, any nontrivial query will be answered with 'undefined'. Not helpful. The only other system I know of is my short theorem prover (on the wiki); it has no architectural reason to not allow list functions, but it has many shallow reasons - slow, obfuscated, doesn't currently track proofs, doesn't currently support higher kinds. Not likely to be usable.