Mercury：如何声明高阶数据类型的确定性？答案

【问题标题】：Mercury: How to declare determinism of a higher-order data type?Mercury：如何声明高阶数据类型的确定性？
【发布时间】：2011-11-14 21:06:40
【问题描述】：

当我编译下面的 Mercury 代码时，我从编译器收到此错误：

In clause for `main(di, uo)':
  in argument 1 of call to predicate
  `test_with_anonymous_functions.assert_equals'/5:
  mode error: variable `V_15' has
  instantiatedness `/* unique */((func) =
  (free >> ground) is semidet)',
  expected instantiatedness was `((func) =
  (free >> ground) is det)'.

我认为编译器的意思是“当您声明类型 test_case 时，您没有指定确定性，所以我假设您的意思是 det。但随后您传入了 semidet lambda。”

我的问题：

声明类型确定性的语法是什么？我尝试过的猜测都导致了语法错误。
有人能解释TestCase 的实例化的/* unique */ 部分是什么意思吗？这会导致给定实例化与预期实例化不匹配吗？
在main 中声明 lambda 是否有更简洁的方法？我对 lambda 的声明与在 lambda 中的代码一样多。

代码：

% (Boilerplate statements at the top are omitted.)

% Return the nth item of a list
:- func nth(list(T), int) = T.
:- mode nth(in,      in)  = out is semidet.
nth([Hd | Tl], N) = (if N = 0 then Hd else nth(Tl, N - 1)).

% Unit testing: Execute TestCase to get the 
% actual value. Print a message if (a) the lambda fails
% or (b) the actual value isn't the expected value.
:- type test_case(T) == ((func) = T).
:- pred assert_equals(test_case(T), T,  string, io.state, io.state).
:- mode assert_equals(in,           in, in,     di,       uo) is det.
assert_equals(TestCase, Expected, Message, !IO) :-
    if   Actual = apply(TestCase), Actual = Expected
    then true % test passed. do nothing.
    else io.format("Fail:\t%s\n", [s(Message)], !IO).

main(!IO) :-
    List = [1, 2, 3, 4],
    assert_equals( ((func) = (nth(List, 0)::out) is semidet),
                 1, "Nth", !IO).

【问题讨论】：

标签： lambda non-deterministic mercury

【解决方案1】：

本是对的，

我想补充一点，Mercury 默认假定函数是确定性的（函数应该是确定性的，这是明智的）。对于必须声明确定性的谓词来说，情况并非如此。这使得使用确定性函数进行高阶编程比任何其他函数或谓词更容易，仅仅是因为样板更少。

因此，您可以使您的 lambda 表达式更加简洁。您还可以通过将头部中的变量 S 替换为主体来将 lambda 表达式的主体移动到头部。

apply_transformer((func(S0) = "Hello " ++ S0),
                  "World", Msg),

【讨论】：

【解决方案2】：

我也花了一段时间才掌握了窍门。

问题在于高阶项的众数不是其类型的一部分。因此，没有用于声明类型确定性的语法。模式中承载了高阶项的确定性。

在您的示例中，assert_equals 的第一个参数的类型为 test_case(T)，但模式为 in。这意味着函数semidet 的事实丢失了。如果您传递的函数是det，我不确定它是否会真正编译或运行正确；即使在那种情况下，模式也不应该是in。

这是一个例子：

:- pred apply_transformer(func(T) = T, T, T).
:- mode apply_transformer(func(in) = out is det, in, out).
apply_transformer(F, X0, X) :-
    X = F(X0).

main(!IO) :-
    apply_transformer((func(S0) = S is det :- S = "Hello " ++ S0),
                      "World", Msg),
    print(Msg, !IO),
    nl(!IO).

如您所见，apply_transformer 的第一个参数的类型仅表示它是一个高阶函数，接受一个参数并返回相同类型的结果。正是模式声明实际上说函数参数的模式为in，函数结果的模式为out，其确定性为det。

我相信错误消息的/*unique */ 位表示编译器认为它是一个唯一值。我不确定这是否有问题，因为除了通常的 io 状态之外，您没有在任何地方使用独特模式。

至于 lambda 语法，不幸的是，我认为你不能做得更好。我发现 Mercury 中 lambda 的语法相当不令人满意。它们太冗长了，以至于我通常只为除了最微不足道的 lambda 之外的所有函数/谓词创建命名函数/谓词。

【讨论】：

谢谢，本。这种解释是有道理的（它解决了我的问题！）
@Evan：我忘了补充我的答案，也可以为高阶项的复杂模式创建模式别名。我曾经为一个具有数十个谓词的模块做过一次，这些谓词采用相同类型的高阶参数；我在模块顶部声明了一个类型和一个模式，并在整个过程中使用了它们。
@Evan: 嘿，你想看看stackoverflow.com/questions/13896296/… -- 和这篇文章无关，只是为了吸引对Evan的关注

【解决方案3】：

为了回答第二个问题，错误消息中的/* unique */ 指的是调用assert_equals 的第一个参数，这是您刚刚构造的lambda 项。这是唯一使用该术语的地方，因此在调用时对其的引用是唯一的。

唯一的 inst 与基础 inst 匹配（但反之亦然），因此在这种情况下，唯一性不会导致不匹配。问题在于决定论。

【讨论】：