haskell - 在 Haskell 中，是否有一种有效的方法来生成给定泛型(尤其是 monads)类型签名的函数？

Question

我已经看到了“给定类型签名 XXX ，在 Haskell 中找到实现”形式的各种问题。因此很自然地会问这是否可以推广或算法化。类似的问题是 here .然而，很明显，通常这项任务是不可能的。所以下一个问题是用一些通用性来换取实用性。

Question: Is the problem decidable if all the type signatures consists of rigid type variables together with some constraints, drawn from a fixed set (e.g. Monad, Traversable, Foldable?)

一个典型的问题是 (Monad m) => (m j -> [m d]) -> m [j] -> [m [d]] ，我使用的地方 []而不是 (..Constraints t) => t为了方便。

Answer 1

令人惊讶的是，这实际上是可能的!看看 Djinn(或者你可以自己编译 the executable)，它为你实现了这个。例如，给定 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 等语言编写的程序等效于证明。例如，为 f :: a -> (a -> b) -> (a -> b -> c) -> c 编写实现等效于证明语句'给定一个命题 a ，那么如果 a 隐含 b ，并且 a 和 b 一起隐含 c ，那么就可以证明这个 67x1 的自动化实现是正确的，因为这个 67x1 的代码可以自动转换为 67x1 的自动化实现。以获得实现。)