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?

Jasisa

ghc --guess-what-i-want-to-do --and-make-me-tea-while-you-re-at-it. After all, given main :: IO () you could generate the whole program. – Filomenafiloplume

Look at Djinn. Basically, yes, it can be done. – Team

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.

Yong

+1 for the link to Djinn. Clearly I'm going to have to study that. I'm mostly interested in whether it can untangle tricky monad transformer problems... – Jasisa

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

Siloum

+1 for more helpful insight. It doesn't surprise me that a given type could have multiple implementations How many ways can you do Int -> Int? Quite a lot, I would think. What's interesting is how often these methods generate useful code... – Jasisa

@MathematicalOrchid, depends on your definition of "useful" :) There are "only" 2^(2^37) functions Int -> Int if Int is 32-bit (or, more generally (2^n)^(2^n) == 2^(n*2^n) if Int is n bits). But there are uncountably many functions Integer -> Integer. Although only a countable number of those are computable. – Siloum

There might be (2^n)^(2^n) distinct functions of type Int -> Int, but I would suggest there are more implementations than that. ;-) And Integer doesn't represent unbounded integers on any physical machine that runs Haskell. If we're going to split hairs... – Jasisa

Out of interest, what's your distinction between a function and an implementation? – Siloum

\ x -> x + 1 + 1 is a different expression from \ x -> x + 2. Yet clearly they are different implementations of what is logically the same function. So there might be X possible input/output mappings over 32-bit integers, but that doesn't mean there's X ways to code it. ;-) – Jasisa

That means that every function has infinitely many implementations: \x -> const (x + 2) <arbitrary expression>. – Siloum

Yes, that was my conclusion also. – Jasisa

Answer 3

This is impossible in general (and for languages like Haskell that does not even has the strong normalization property), and only possible in some (very) special cases (and for more restricted languages), such as when a codomain type has the only one constructor (for example, a function f :: forall a. a -> () can be determined uniquely). In order to reduce a set of possible definitions for a given signature to a singleton set with just one definition need to give more restrictions (in the form of additional properties, for example, it is still difficult to imagine how this can be helpful without giving an example of use).

From the (n-)categorical point of view types corresponds to objects, terms corresponds to arrows (constructors also corresponds to arrows), and function definitions corresponds to 2-arrows. The question is analogous to the question of whether one can construct a 2-category with the required properties by specifying only a set of objects. It's impossible since you need either an explicit construction for arrows and 2-arrows (i.e., writing terms and definitions), or deductive system which allows to deduce the necessary structure using a certain set of properties (that still need to be defined explicitly).

---

There is also an interesting question: given an ADT (i.e., subcategory of Hask) is it possible to automatically derive instances for Typeable, Data (yes, using SYB), Traversable, Foldable, Functor, Pointed, Applicative, Monad, etc (?). In this case, we have the necessary signatures as well as additional properties (for example, the monad laws, although these properties can not be expressed in Haskell, but they can be expressed in a language with dependent types). There is some interesting constructions:

http://ulissesaraujo.wordpress.com/2007/12/19/catamorphisms-in-haskell

which shows what can be done for the list ADT.

Pharmacy

Answer 4

The question is actually rather deep and I'm not sure of the answer, if you're asking about the full glory of Haskell types including type families, GADT's, etc.

What you're asking is whether a program can automatically prove that an arbitrary type is inhabited (contains a value) by exhibiting such a value. A principle called the Curry-Howard Correspondence says that types can be interpreted as mathematical propositions, and the type is inhabited if the proposition is constructively provable. So you're asking if there is a program that can prove a certain class of propositions to be theorems. In a language like Agda, the type system is powerful enough to express arbitrary mathematical propositions, and proving arbitrary ones is undecidable by Gödel's incompleteness theorem. On the other hand, if you drop down to (say) pure Hindley-Milner, you get a much weaker and (I think) decidable system. With Haskell 98, I'm not sure, because type classes are supposed to be able to be equivalent to GADT's.

With GADT's, I don't know if it's decidable or not, though maybe some more knowledgeable folks here would know right away. For example it might be possible to encode the halting problem for a given Turing machine as a GADT, so there is a value of that type iff the machine halts. In that case, inhabitability is clearly undecidable. But, maybe such an encoding isn't quite possible, even with type families. I'm not currently fluent enough in this subject for it to be obvious to me either way, though as I said, maybe someone else here knows the answer.

(Update:) Oh a much simpler interpretation of your question occurs to me: you may be asking if every Haskell type is inhabited. The answer is obviously not. Consider the polymorphic type

a -> b

There is no function with that signature (not counting something like unsafeCoerce, which makes the type system inconsistent).

Alsatian

AFAIK, H98 is based on HM and decidable (type classes without fundeps is simply desugared), GHC system is based on SystemFC and undecidable (there is possible to write LC in type level and then write unterminated term in it). – Pharmacy

To be pedantic, every type in Haskell is inhabited (the type system is already inconsistent) e.g. by undefined. Usually when we ask a question like this, we want total values, but then we have to be careful what we mean by that, because e.g. fix is not total, but is certainly quite an interesting function; is [1 ..] total? Is the type data Stream a = Cons a (Stream a) inhabited? – Roseline

Also, there is a functions like f :: t; f = f which can be used like undefined (such functions are not possible in HM or in SystemF, since they violate the strong normalization property). – Pharmacy

Sure, I realise that all this interesting theory only applies to Haskell "if you don't cheat". We have infinite loops, exceptions, unsafeCoerce, FFI... – Jasisa