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

本文介绍了给定 Haskell 类型签名，是否可以自动生成代码?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

标题中的内容.如果我写一个类型签名，是否可以通过算法生成具有该类型签名的表达式?

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?

似乎有可能做到这一点.我们已经知道，如果类型是库函数类型签名的特例，Hoogle 可以通过算法找到该函数.另一方面，许多与一般表达式相关的简单问题实际上是无法解决的(例如，不可能知道两个函数是否做同样的事情)，因此很难说这是其中之一.

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 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 做了这是 Haskell 类型的受限子集，对应于一阶逻辑.但是，它无法管理递归类型或需要递归实现的类型；因此，例如，它不能编写 (a -> a) -> 类型的术语.a(fix 的类型)，对应于命题if a 蕴含 a，则 a"，这显然是错误的；你可以用它来证明任何事情.事实上，这就是为什么 fix 会产生 ⊥.

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

如果你do允许fix，那么编写一个程序来给出任何类型的术语是微不足道的；该程序将简单地为每种类型打印fix id.

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 主要是一个玩具，但它可以做一些有趣的事情，比如为 Reader 和 Cont 派生正确的 Monad 实例，给定return 和 (>>=) 的类型.您可以通过安装 djinn 包或使用 lambdabot，将其集成为 @djinn 命令.

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.