Tre*_*bor 5 haskell type-theory hindley-milner
我已经看到了“给定类型签名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，那么如果a暗示b，并a和b一起暗示c，那c是真实的。”正因为如此，你可以使用自动标定找出执行，然后只是机械地转换成代码此得到实现。）