汞清单统一答案

【问题标题】：Mercury List Unification汞清单统一
【发布时间】：2019-03-02 10:32:53
【问题描述】：

我正在努力学习Mercury。我一直在搞乱列表，但我无法让看似简单的统一工作。这是我的简化示例：

main(!IO) :-
  [X,Y] = List,
  List = [1,2], % Error
  io.write(List, !IO),
  io.nl(!IO).

在List = [1,2] 行我收到以下错误（格式化并稍作编辑）：

main.m:024: In clause for `main(di, uo)':
mode error in unification of `List' and `list.[V_11 | V_21]'.
Variable `List' has instantiatedness
`unique(list.'[|]'(free, unique(list.'[|]'(free, unique((list.[]))))))', 
term `list.[V_11 | V_21]' has instantiatedness
`list.'[|]'( unique(1), free )'.

不过，这似乎不对；特别是[1,2] 的实例化。这是一个字面意思；它的实例化不应该是list.'[|]'( unique(1), list.'[|]'( unique(2), [] ) )吗？

这是否与 here 相同的部分实例化问题有关？

【问题讨论】：

标签： mercury

【解决方案1】：

为了编译一个模式正确的程序，Mercury 会在一个合相中重新排序目标，以尝试制作一个模式正确的程序，但在它这样做之前，它还会将复杂的 unfications 分解成多个部分。看起来 Mercury 正在努力重新排序这两个统一的部分以制作一个模式正确的程序，即使（从我看来）它应该是可能的。尝试重新排列前两个目标。

【讨论】：

是的，重新排序这两行可以解决问题。但是，这实际上并不能解决我的问题，因为这只是对更复杂的用例的简化；我希望能够声明一个未知列表，然后在其中统一值。与此同时，我在 Prolog 中尝试了它，虽然语法有时很烦人，但它主要是在做我想做的事。如果 Mercury 也能做到，那就太好了。
旁注：如果我保留问题中给出的两行，但写X和Y而不是List，我会收到以下错误，而不是：main.m： 059：在__Unify__'((unique((list.[])) >> bound((list.[]))), (bound((list.[])) >> bound((list.[])))): error: implicit determinism declaration not satisfied. Declared det'中，推断semidet'. Unification of CastY'和'CastX'可能会失败。
@Erhannis：“声明一个未知列表，然后在其中统一值”：不，这在 Mercury 中仍然不起作用。（见Q1 here。）
@TomasBy 啊，真可惜。你知道相关功能是否正在开发中，或者我要去哪里问？
@Erhannis：我强烈怀疑它是否正在开发中。你可以在mailing list问。