问题描述
当我发现Mercury编程语言的about page的一部分内容时说:
水星是一种强模式语言
这是什么意思!?我已经在整个互联网上搜索,但没有找到答案!
解决方法
我不知道Mercury中使用的其他任何modes
语言。以下摘自汞手册
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.
如果您熟悉序言,您可能知道这意味着什么。
考虑使用以下typedecl
在 C 中创建函数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,b]).
X = [],Y = [1,b] ;
X = [1],Y = [2,b] ;
X = [1,Y = [a,a],Y = [b] ;
X = [1,Y = [] ;
false.
此append([1],[2],[3]).
失败,而append([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) is semidet.
如果提供前两个,则确定地确定输出。如果提供最后一个参数,则您对前两个参数有多种解决方案。如果您提供全部三个列表,那么它只是检查是否在添加前两个列表时获得了第三个列表。
模式不限于进出。处理IO时,您会看到di
破坏性输入和uo
唯一输出。他们只是告诉我们谓词如何改变我们提供的参数实例。输出从自由变量变为基本项,而输入保持基本项。因此,作为用户,您可以定义:- mode input == ground >> ground.
和:- mode output == free >> ground.
并使用它们,这正是定义in
和out
模式的方式。
考虑一个谓词,该谓词计算列表的长度。我们不需要实例化整个列表,因为我们知道length([X,Y],2)是正确的,即使X,Y是自由变量也是如此。因此,模式声明:- mode length(in,out) is det.
不足,因为不需要实例化整个第一个参数。所以我们也可以定义参数的实例化
:- inst listskel == bound([] ; [free | listskel]).
指出如果参数为空列表或在另一个listskel
列表之前的自由变量,则实例化参数listskel
。
由于haskell的惰性,这种部分评估也会发生,例如,无需评估整个列表就可以知道其长度。
参考: modes determinism
编辑:来自汞网站
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).
模式指定数据流的方向,例如输入或输出。
在某些语言中,数据流的方向是固定的,并且隐含在语法中。例如,在大多数函数式语言中,函数参数总是 输入,始终输出函数结果。
然而,在大多数逻辑编程语言中,数据流的方向是在运行时确定的。大多数逻辑编程语言都是动态建模的。
在 Mercury 中,必须声明数据流的方向,至少在模块边界处。但是,Mercury 中的单个谓词或函数可以有多种模式;编译器在编译时解析模式,并为每种模式生成单独的代码。
Mercury 还支持带有约束求解的可选动态模式。
(见https://www.researchgate.net/publication/220802747_Adding_Constraint_Solving_to_Mercury。)
但默认是静态模式。