Given a Haskell type signature, is it possible to generate the code automatically?

Question

What it says in the title. If I write a type signature, is it possible to algorithmically generate an expression which has that type signature?

It seems plausible that it might be possible to do this. We already know that if the type is a special-case of a library function's type signature, Hoogle can find that function algorithmically. On the other hand, many simple problems relating to general expressions are actually unsolvable (e.g., it is impossible to know if two functions do the same thing), so it's hardly implausible that this is one of them.

It's probably bad form to ask several questions all at once, but I'd like to know:

• Can it be done?

• If so, how?

• If not, are there any restricted situations where it becomes possible?

• It's quite possible for two distinct expressions to have the same type signature. Can you compute all of them? Or even some of them?

• Does anybody have working code which does this stuff for real?

Answer 1

Djinn does this for a restricted subset of Haskell types, corresponding to a first-order logic. It can't manage recursive types or types that require recursion to implement, though; so, for instance, it can't write a term of type (a -> a) -> a (the type of fix), which corresponds to the proposition "if a implies a, then a", which is clearly false; you can use it to prove anything. Indeed, this is why fix gives rise to ⊥.

If you do allow fix, then writing a program to give a term of any type is trivial; the program would simply print fix id for every type.

Djinn is mostly a toy, but it can do some fun things, like deriving the correct Monad instances for Reader and Cont given the types of return and (>>=). You can try it out by installing the djinn package, or using lambdabot, which integrates it as the @djinn command.

Answer 2

Oleg at okmij.org has an implementation of this. There is a short introduction here but the literate Haskell source contains the details and the description of the process. (I'm not sure how this corresponds to Djinn in power, but it is another example.)

---

There are cases where is no unique function:

fst', snd' :: (a, a) -> a fst' (a,_) = a snd' (_,b) = b 

Not only this; there are cases where there are an infinite number of functions:

list0, list1, list2 :: [a] -> a list0 l = l !! 0 list1 l = l !! 1 list2 l = l !! 2 -- etc.  -- Or  mkList0, mkList1, mkList2 :: a -> [a] mkList0 _ = [] mkList1 a = [a] mkList2 a = [a,a] -- etc. 

(If you only want total functions, then consider [a] as restricted to infinite lists for list0, list1 etc, i.e. data List a = Cons a (List a))

In fact, if you have recursive types, any types involving these correspond to an infinite number of functions. However, at least in the case above, there is a countable number of functions, so it is possible to create an (infinite) list containing all of them. But, I think the type [a] -> [a] corresponds to an uncountably infinite number of functions (again restrict [a] to infinite lists) so you can't even enumerate them all!

(Summary: there are types that correspond to a finite, countably infinite and uncountably infinite number of functions.)