问题标签 [unification]

编辑：解决。我不知道在源文件中启用语言扩展名并没有在 GHCi 中启用语言扩展名。解决方案是:set FlexibleContexts在 GHCi 中。

我最近发现 Haskell 中的类和实例中的类型声明是 Horn 子句。所以我将 Prolog 的艺术第 3 章中的算术运算编码到 Haskell 中。例如：

在 Prolog 中，为证明中的（逻辑）变量实例化值。但是，我不明白如何在 Haskell 中实例化类型变量。也就是说，我不明白 Prolog 查询的 Haskell 等价物是什么

是。我假设

会导致 Haskell 实例化xi，但这会产生Non type-variable argument in the constraint错误，即使FlexibleContexts启用。

我期待

是否存在一些“优先级”问题？我正在使用最后一个 swi-prolog 版本。

假设我有一个替换S并列出Xs ，其中出现在Xs中的每个变量也出现在S中。我如何找到列表S(Xs)，即通过将替换S应用于列表Xs获得的列表。

更具体地说，我有一组谓词和 DCG 规则，看起来像

如果我尝试将模式P与变量与列表匹配，我会收到替换S：

我想将替换S = {X = c, Y = e}应用于具有变量X和Y的列表Xs，并接收带有替换的列表，但我不确定解决问题的最佳方法是什么.

如果我在 Haskell 中解决这个问题，我会构建一个从变量到值的有限映射，然后执行替换。等效的方法是在 DCG 规则中生成一个变量和值对的列表，然后使用该映射找到所需的列表。然而，这不是一个合适的方法。

我最近在 Mercury 中遇到了这个代码示例：

= 作为一名 Prolog 程序员，我想知道：正常的统一和这里使用的:=or有什么区别？=>

在Mercury 参考文献中，这些运算符获得不同的优先级，但它们没有解释差异。

我正在阅读Haskell 中的 Typed Logical Variables论文，但我无法理解最终实现的细节。特别是第 4 节中介绍的回溯状态转换器。出于某种我不知道的原因，GHC 认为我需要在函数中的MonadPlus实例，如下所示：(ST a)unify

我不确定问题是什么，以及如何解决它。到目前为止，我的印象是我理解了前面的讨论和代码，但显然我错了。如果有人能指出出了什么问题——我是否需要一个MonadPlus (ST a)实例？- 这将非常有帮助。

[编辑：澄清]我应该指出，作者似乎声称mzero或 的某些变体mzero是适当的功能。我只是不知道合适的功能是什么。我想知道是我应该创建一个MonadPlus (ST a)实例还是我没有使用正确的功能，并且误读了一些东西。

我写了以下函数：

但是当我尝试编译时出现以下错误：

任何人都可以帮忙吗？

可能重复：
Prolog 删除：不删除与 Element 统一的所有元素

在 Prolog 中，如果你这样写：

结果将是：

这是正常的，因为 _ 变量在第一个元素中与 1 绑定，它会搜索 (1,1) 的其他元素并删除它们。

有没有办法防止这种统一发生并删除表单（1，_）的所有成员。在这种情况下，结果必须是：L = [ (3, 4)]。

有人可以解释Prolog中的==和运算符之间的区别吗？=我知道这X = Y意味着 X 与 Y 统一，并且如果 X 已经与 Y 统一或可以做到，则为真，但我不明白这与==.

跟进：那（见接受的答案）是有道理的。还有一个问题，是否存在X \= Y真假X \== Y（反之亦然）的情况？也就是说，是否X \= Y测试它们是否无法统一或当前是否不统一？

所以在这里，对于我的数独项目，我有一个列表，例如：

我想过滤它以仅获取自由变量：

所以想要那个，我写了这个谓词：

打电话时

SWI-Prolog 答案

所以我稍微编辑了谓词：

现在它按预期工作：

尽管如此，我还是看不出第一个有什么问题，对我来说，SWI-Prolog 应该将 0:0:0 与 _ 以及与 _:_:_ 匹配。有什么我没有得到的吗？或者它是一个 SWI-Prolog 错误？

感谢您的任何启发！

我正在转换 AST，需要的不仅仅是简单的模式匹配，因此需要统一算法。

虽然这是针对 .NET 项目的，而且我知道我可以与 .NET PROLOG 实现互操作，但我只需要嵌入统一算法；所以PROLOG是矫枉过正的。

如果我能得到用 F# 编写的“Martelli, Montanari: An Efficient Unification Algorithm”，那将是完美的，但我会接受任何功能语言，包括 HASKELL 并翻译成 F#。