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 then I want to ask, say, for a program of type [Int] -> Bool and get as answer (fold and True) . (map isZero) I have found two approaches in this direction. The first one is the De-Typechecker http://www.haskell.org/pipermail/haskell/2005-March/015423.html and the other one is Djinn http://permalink.gmane.org/gmane.comp.lang.haskell.general/12747 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? Regards, Klaus
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.
Hi,
I have got loads of requests to allow Hoogle to do this, usually
something like if you search [Bool] -> [Bool] it should suggest map
not, or something - combining functions into the one you want.
Unfortunately the search space would be huge for even the smallest
library. Worse still, the second you allow id :: a -> a, you have an
infinite number of matching terms.
Some work I have seen which seems related to what you are asking is:
http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/14num.pdf "Systematic
search for lambda expressions" by Susumu Katayama.
Thanks
Neil
On 1/28/07, Stefan O'Rear
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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Klaus Ostermann -
Neil Mitchell -
Stefan O'Rear