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 <[EMAIL PROTECTED]> wrote:
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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
