我已经看到了各种形式的问题“给定类型签名XXX，在 Haskell 中找到实现”。因此很自然地要问这是否可以概括或算法化。一个类似的问题是here。但是，很明显，通常这项任务是不可能的。所以下一个问题是用一些通用性换取实用性。
问题：如果所有类型签名都由刚性类型变量和一些约束组成，那么问题是否可以确定，这些约束是从一个固定的集合中提取的（例如
Monad, Traversable, Foldable？）
一个典型的问题是，为了方便起见(Monad m) => (m j -> [m d]) -> m [j] -> [m [d]]，我使用了它[]而不是。(..Constraints t) => t
令人惊讶的是，这实际上是可能的！看看Djinn（或者你可以自己编译可执行文件），它为你实现了这个。例如，给定f :: a -> (a -> b) -> (a -> b -> c) -> c，Djinn 输出f a b c = c a (b a)（以及其他可能性）。您可以在http://lambda-the-ultimate.org/node/1178找到更多示例（使用命令行版本）。不幸的是，虽然它不支持类型类，但我不排除我还没有找到支持它们的另一个工具。
（如果你对它的工作原理感兴趣，请阅读Curry-Howard Isomorphism，它指出用 Haskell 等语言编写的程序等同于证明。例如，为 for 编写实现f :: a -> (a -> b) -> (a -> b -> c) -> c等同于证明陈述'给定一个命题a，然后 ifa暗示b，并且a和b一起暗示c，c则为真'。因此，您可以使用自动证明者来计算实现，然后将其机械地翻译成代码以获得实现。）