[Haskell-cafe] Converting Types to Terms
Stefan O'Rear
stefanor at cox.net
Sun Jan 28 15:33:53 EST 2007
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.
More information about the Haskell-Cafe
mailing list