[Haskell-cafe] Converting Types to Terms

[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.