[Haskell-cafe] Converting Types to Terms

[Neil Mitchell]

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 <stefanor at cox.net> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>