给定一个Haskell类型签名，是否可以自动生成代码？ [英] Given a Haskell type signature, is it possible to generate the code automatically?
问题描述
标题中说了什么。如果我写了一个类型签名，是否有可能通过算法生成一个具有该类型签名的表达式？
似乎有可能做到这一点。我们已经知道，如果类型是库函数类型签名的特例，Hoogle可以通过算法找到该函数。另一方面，与通用表达式有关的许多简单问题实际上是无法解决的（例如，不可能知道两个函数是否执行相同的操作），所以这是其中的一个难以置信的。
一次提出几个问题可能是不好的形式，但我想知道： 如果是这样，怎么做？ If不，是否有任何限制的情况发生？ 两个不同的表达式很可能具有相同的类型签名。你能计算它们的全部吗？甚至是 ？
Djinn 对Haskell类型的一个受限子集做了这个操作，这对应于一阶逻辑。尽管如此，它不能管理需要递归实现的递归类型或类型;所以，例如，它不能写出（a - > a） - >一个（类型 fix ），它与命题if a 暗示 a ，然后是 a ，这显然是错误的;你可以用它来证明任何事情。事实上，这就是为什么 fix 引起⊥。
如果您允许允许修复，然后编写一个程序来给出任何类型的术语是微不足道的;该程序只需为每种类型打印 fix id 。
Djinn主要是玩具，但它可以做一些有趣的事情，例如为 Reader 和 Cont Monad 实例c>给出 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.
这篇关于给定一个Haskell类型签名，是否可以自动生成代码？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
