如何像在 Prolog 中一样在 Mercury 中生成新变量列表？

Question

在 SWI Prolog 中，list(Xs) :- length(Xs, _).是“纯”的，因为我可以向它传递一个具有任何类型实例化的变量，并且它将非确定性地将它与特定长度的所有最通用的统一词统一起来。

是否可以list/1在水星中写一个纯？该手册似乎暗示可以做到这一点，但我在实际实施时遇到了麻烦。

到目前为止我所拥有的是：

:- module mylist.

:- interface.

:- import_module list.

:- inst frees for list/1
    --->    []
    ;       [free | frees].
:- mode free_to_frees == free >> frees.

:- pred mylist(list(_)).
:- mode mylist(in) is det.
:- mode mylist(free_to_frees) is multi.

:- implementation.

:- pragma promise_pure(mylist/1).

mylist(_::in).

mylist([]::free_to_frees).
mylist([_|Xs]::free_to_frees) :- mylist(Xs).

但是，当我尝试这样做时：

:- module main.
:- interface.
:- implementation.
:- import_module list, mylist.

:- pred getlist(list(int)).
:- mode getlist(free >> ground) is multi.
getlist(Xs) :- Xs = [1, 2, 3].
getlist(Xs) :- mylist(Xs), Xs = [5].

我收到以下错误：

main.m:011: In clause for `getlist(out)':
main.m:011:   mode error in conjunction. The next 2 error messages indicate
main.m:011:   possible causes of this error.
main.m:011:   
main.m:011:   In clause for `getlist(out)':
main.m:011:   mode error in unification of `Xs' and `list.[V_10 | V_16]'.
main.m:011:   Variable `Xs' has instantiatedness
main.m:011:     bound(
main.m:011:       []
main.m:011:     ;
main.m:011:       '[|]'(
main.m:011:         free,
main.m:011:         named inst mylist.listskel,
main.m:011:         which expands to
main.m:011:           bound(
main.m:011:             []
main.m:011:           ;
main.m:011:             '[|]'(
main.m:011:               free,
main.m:011:               named inst mylist.listskel
main.m:011:             )
main.m:011:           )
main.m:011:       )
main.m:011:     ),
main.m:011:   term `list.[V_10 | V_16]' has instantiatedness
main.m:011:   `named inst list.'[|]'(unique(5), free)'.
main.m:011:   
main.m:011:   In clause for `getlist(out)':
main.m:011:   in argument 1 of clause head:
main.m:011:   mode error in unification of `HeadVar__1' and `Xs'.
main.m:011:   Variable `HeadVar__1' has instantiatedness `free',
main.m:011:   variable `Xs' has instantiatedness
main.m:011:     bound(
main.m:011:       []
main.m:011:     ;
main.m:011:       '[|]'(
main.m:011:         free,
main.m:011:         named inst mylist.listskel,
main.m:011:         which expands to
main.m:011:           bound(
main.m:011:             []
main.m:011:           ;
main.m:011:             '[|]'(
main.m:011:               free,
main.m:011:               named inst mylist.listskel
main.m:011:             )
main.m:011:           )
main.m:011:       )
main.m:011:     ).

我猜我的使用free可能不正确，否则我需要添加一个额外的模式或概括我的listskelinst 以涵盖mylist(Xs), Xs = [5].

基本上，我应该如何写mylist/1，以便它可以在尽可能多的模式下使用？

谢谢！

Answer 1

由于 Mercury 实施的限制（记录在 Mercury 发行版的 LIMITATIONS 文件中），您的要求无法完成。

虽然 Mercury 语言的设计允许描述部分实例化术语的模式，例如自由变量列表，例如 的预期输出mylist(Xs)，但这些术语没有用，除非您可以对它们做一些事情，例如将它们与 统一[5]。由于 Mercury 编译器需要知道所有程序点上所有变量的实例化状态，因此只有当它能够跟踪自由变量与其他自由变量之间的所有统一时（无论它们是否出现在这些术语中），它才能允许这样做）。这是因为如果你有统一A = B, B = C, and C = D, 然后你统一D了5，编译器需要知道这不仅基于D， 而且A，B和C以及。这是因为这些unifications取得A，B和C 别名 的D（也就是说，它们是其他的方式来指代D）。

当 Mercury 在 1990 年代中期首次实施时，我们有一名学生从事别名跟踪工作。不幸的是，他发现虽然别名跟踪是可能的，但它是不可行的，因为它打开别名跟踪通常至少翻倍编译模块所需的时间。我们认为，为几乎从未使用过的功能付出的代价太高了。即使今天，由于摩尔定律，别名跟踪的绝对成本会小得多，相对的权衡并没有真正改变，我们现在有几十年的与水星合作的经验，我们发现很少在这种情况下，支持填充部分实例化的数据结构会很有用，但我一时想不起来了。

在 Mercury 中编程与在 Prolog 中编程有很大不同。这是设计使然。在 Mercury 中，您无需构建部分实例化的术语然后再填充它，而只需直接构建最终术语。对于任何对程序可靠性感兴趣的程序员，即使在 Prolog 中工作时，这也是首选的操作过程。在真正的 Prolog 程序中，与解谜或学生练习相反，未实例化的术语的一部分更可能是错误。