5

我正在浏览 Mercury 编程语言的about 页面时，我发现它说：

Mercury 是一种强模式语言

这是什么意思！？我在整个互联网上搜索，但没有找到答案！

4

2 回答 2

6

我不知道modes在 Mercury 中使用过的任何其他语言。以下来自水星手册

The mode of a predicate (or function) is a mapping from the initial
state of instantiation of the arguments of the predicate (or the
arguments and result of a function) to their final state of
instantiation.

如果您熟悉 prolog，您可能知道这意味着什么。

考虑C中具有以下 typedecl的函数

void sort(int * i, int * o);

假设此函数将数组排序i到另一个数组o中。仅仅从这个声明中，我们不能保证i读取和o写入。如果我们可以另外编写mode sort(in, out)，则向编译器建议函数 sort 从第一个参数读取并写入第二个参数。然后编译器检查函数体以向我们保证不会发生写入i和读取o。

对于这样的语言C可能不适合，但对于prolog家庭语言，这是一个非常受欢迎的功能。考虑append/3当连接的前两个列表是第三个列表时成功的谓词。

append([1, 2], [a, b], X).
X = [1, 2, a, b]

因此，如果我们提供两个输入列表，我们将得到一个输出列表。但是当我们提供输出列表并询问所有导致它的解决方案时，我们有

append(X, Y, [1, 2, a, b]).
X = [],
Y = [1, 2, a, b] ;
X = [1],
Y = [2, a, b] ;
X = [1, 2],
Y = [a, b] ;
X = [1, 2, a],
Y = [b] ;
X = [1, 2, a, b],
Y = [] ;
false.

这在 as成功的append([1], [2], [3]).地方失败了。append([1], [2], [1, 2]).因此，根据我们如何使用谓词，我们可以有一个确定性答案、多个答案或根本没有答案。谓词的所有这些属性最初都可以通过模式声明来声明。以下是 的模式声明append：

:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out) is det.
:- mode append(out, out, in) is multi.
:- mode append(in, in, in) is semidet.

如果您提供前两个，则输出是确定性确定的。如果您提供最后一个参数，那么您对前两个参数有多种解决方案。如果您提供所有三个列表，那么它只会检查当前两个附加时我们是否得到第三个列表。

模式不限于进出。在处理 IO 时，您会看到di破坏性的输入和独特的输出。uo它们只是告诉我们谓词如何改变我们提供的参数的实例化。输出从自由变量变为基本项，输入仍然是基本项。因此，作为用户，您可以定义:- mode input == ground >> ground.和:- mode output == free >> ground.使用它们，这正是定义的方式in和out模式。

考虑一个计算列表长度的谓词。我们不需要实例化整个列表，因为我们知道即使 X, Y 是自由变量，length([X, Y], 2) 也是正确的。所以模式声明:- mode length(in, out) is det.是不够的，因为不需要实例化整个第一个参数。因此，我们还可以定义参数的实例化性， :- inst listskel == bound([] ; [free | listskel]). 即如果参数是listskel空列表或另一个listskel列表之前的自由变量，则该参数被实例化。

由于 Haskell 的惰性，这种部分评估也发生在 Haskell 中，例如，不需要评估整个列表即可知道其长度。

参考： 模式 决定论

编辑：来自水星网站 Currently only a subset of the intended mode system is implemented. This subset effectively requires arguments to be either fully input (ground at the time of call and at the time of success) or fully output (free at the time of call and ground at the time of success).

于 2020-11-05T04:49:37.707 回答
1

模式指定数据流的方向，例如输入或输出。

在某些语言中，数据流的方向是固定的，并且隐含在语法中。例如，在大多数函数式语言中，始终输入函数参数，始终输出函数结果。

然而，在大多数逻辑编程语言中，数据流的方向是在运行时确定的。大多数逻辑编程语言都是动态建模的。

在 Mercury 中，必须声明数据流的方向，至少在模块边界处。但是，Mercury 中的单个谓词或函数可以有多种模式。编译器在编译时解析模式，并为每种模式生成单独的代码。

Mercury 还支持具有约束求解的可选动态模式。（参见https://www.researchgate.net/publication/220802747_Adding_Constraint_Solving_to_Mercury。）
但默认是静态模式。

于 2021-02-25T01:16:43.810 回答