给定一个Haskell类型签名，是否可以自动生成代码？

Djinn 对Haskell类型的一个受限子集做了这个操作，这对应于一阶逻辑。尽管如此，它不能管理需要递归实现的递归类型或类型;所以，例如，它不能写出（a - > a） - >一个（类型 fix ），它与命题if a 暗示 a ，然后是 a ，这显然是错误的;你可以用它来证明任何事情。事实上，这就是为什么 fix 引起⊥。

如果您允许允许修复，然后编写一个程序来给出任何类型的术语是微不足道的;该程序只需为每种类型打印 fix id 。

Djinn主要是玩具，但它可以做一些有趣的事情，例如为 Reader 和 Cont 给出 return 和（>> =）的类型。您可以尝试安装 djinn 软件包，或者使用 lambdabot ，该它集成作为 @djinn 命令。

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?

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.