我已经看到了“给定类型签名 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
为了方便。
最佳答案
令人惊讶的是,这实际上是可能的!看看 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 的自动化实现。以获得实现。)
关于haskell - 在 Haskell 中,是否有一种有效的方法来生成给定泛型(尤其是 monads)类型签名的函数?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59216254/