什么是“强模式”编程语言？

Question

我正在浏览 Mercury 编程语言的关于页面时，发现其中有一段内容：

Mercury 是一种强模式化的语言

这是什么意思！？我在互联网上搜索了所有内容，都没有找到答案！

Answer 1

我不知道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的函数

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.

假设此函数将数组排序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.

这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 中，例如，不需要评估整个列表以了解其长度。

参考资料： 模式 决定论

编辑：来自汞网站 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).