在Prolog中进行更安全类型的测试

Question

ISO-Prolog（ISO/IEC 13211-1:1995，包括Cor.1:2007，Cor.2:2012）提供了用于测试术语类型的以下内置谓词：

8.3 类型测试

1 var/1. 2 atom/1. 3 integer/1. 4 float/1. 5 atomic/1. 6 compound/1. 7 nonvar/1. 8 number/1. 9 callable/1. 10 ground/1. 11 acyclic_term/1.

在这个组中，有些谓词的目的仅仅是为了测试特定的实例化，即8.3.1 var/1，8.3.7 nonvar/1，8.3.10 ground/1，以及那些假设术语已经被充分实例化以使类型测试安全的谓词。不幸的是，它们与对具体实例化的测试结合在一起。

考虑目标integer(X)，如果X是一个非变量且不是整数的非变量项并且X是一个变量时失败。这破坏了许多理想的声明性质：

?- X = 1, integer(X).
   true.
?- integer(X), X = 1.
   false.

理想情况下，第二个查询要么通过某种协程形式成功执行；要么根据error classification发出实例化错误¹。毕竟：

7.12.2 错误分类

错误按照Error_term的形式进行分类：

a) 当参数或其组件为变量且需要已实例化的参数或组件时，会出现实例化错误。它的形式为instantiation_error。

...

请注意，这种隐含的实例化测试和类型测试的组合会导致Prolog程序中的许多错误，也会在此处发生。

对这种情况的快速修复是在每个测试内置之前添加显式测试，可以如下详细描述：

   ( nonvar(T) -> true ; throw(error(instantiation_error,_)) ),
   integer(T), ....

更简洁地说，可以表示为

functor(T, _,_),
integer(T), ....

它甚至可能更好。

T =.. _,
integer(T), ...

我的问题有两个方面：

如何在用户级别提供此功能？

以及，为了使其更具挑战性：

什么是使用ISO-Prolog编写的更紧凑的、更安全的atomic/1实现？

---

其他不太理想的选择是循环或产生资源错误。但仍然比得到错误结果要好。

- false

---

must_be(integer, X) 如何适用于此（只是举个例子）？ - user1812457

@Boris：must_be(integer, a) 会产生一个 type_error(integer,a) - 它应该失败。 - false

@false。我不理解你上面的评论（1月8日，12:50）。为什么must_be(integer,a)应该失败？根据手册页面，must_be从不失败。可能是其他谓词会失败。（如has_type/2，如果我没记错的话） - repeat

@repeat: 产生错误的类型测试不能用于编程纯谓词，因为您需要使用catch/3捕获错误。如果有替代方案，类型错误是无用的，只有在您说TINA时才有用。 - false

@David：对于integer(X)的回答为false意味着没有整数。integer(X)失败的原因是DEC10没有错误，而它的前身（马赛）Prolog I有错误，但是没有人读过（法国）论文。 - false

Answer 1

对于类型的测试需要与传统的“类型测试”内置函数区分开来，后者隐式地还会测试是否有足够的实例化。因此，我们只对已充分实例化的术语（si）进行有效测试。如果它们没有被充分实例化，则会发出适当的错误。

对于类型nn，因此存在一个类型测试谓词nn_si/1，其唯一的错误条件是：

a) 如果存在θ和σ使得nn_si(Xθ)为真且nn_si(Xσ)为假
— instantiation_error。

atom_si(A) :-
   functor(A, _, 0),    % for the instantiation error
   atom(A).

integer_si(I) :-
   functor(I, _, 0),
   integer(I).

atomic_si(AC) :-
   functor(AC,_,0).

list_si(L) :-
   \+ \+ length(L, _),  % for silent failure
   sort(L, _).          % for the instantiation error

character_si(Ch) :-
   functor(Ch,Ch,0),
   atom(Ch),
   atom_length(Ch,1).

chars_si(Chs) :-
   \+ \+ length(Chs,_),
   \+ ( once(length(Chs,_)), member(Ch,Chs), nonvar(Ch), \+ character_si(Ch) ),
   \+ ( member(Ch,Chs), \+ character_si(Ch) ). % for the instantiation error

在Scryer中，可以使用library(si)来获取此功能。

在SWI中，由于其在length/2上的行为不同，请使用以下方法：

list_si(L) :-
    '$skip_list'(_, L, T),
    functor(T,_,_),
    T == [].

- false

---

@j4nbur53: 动机是：throw/1需要为error/2的第二个参数提供一些值。然而，该值是实现定义的，这意味着必须为每个实现指定一个特定的值。甚至_也不行。 - false

@j4nbur53：非常好的观点。上述代码假设系统符合规范。 - false

你的观察对于SICStus是不准确的：直到最近，它在throw(error(type_error(list,1),_)).中产生了一个实例化错误。现在，它会直接显示错误术语，而_=..1.则会产生一个格式良好的错误。 - false

我看不出error(instantiation_error,functor/3)有什么误导性。无论如何，这里只有第一个参数是相关的... - false

@j4nbur53：那不相关：只有error/2的第一个参数是有意义的。 - false

Answer 2

这是一个非常幼稚的尝试，旨在实现您提出的两种解决方案。

首先，has_type(Type, Var) 要么成功，要么失败并出现实例化错误：

has_type(Type, X) :-
    var(X), !,
    throw(error(instantiation_error, _)).
has_type(Type, X) :-
    nonvar_has_type(Type, X).

nonvar_has_type(atom, X) :- atom(X).
nonvar_has_type(integer, X) :- integer(X).
nonvar_has_type(compound, X) :- compound(X).
% etc

第二，一个could_be(Type, Var)（类似于must_be/2）使用协程使查询在未来某个时间点成功：

could_be(Type, X) :-
    var(X), !,
    freeze_type(Type, X).
could_be(Type, X) :-
    nonvar_has_type(Type, X).

freeze_type(integer, X) :- freeze(X, integer(X)).
freeze_type(atom, X) :- freeze(X, atom(X)).
freeze_type(compound, X) :- freeze(X, compound(X)).
% etc

这种方法存在一些弱点，但您的评论可能会帮助我更好地理解用例。

编辑：Prolog中的“类型”

就我所理解的Prolog中的类型而言，并不是“类型”：它们只是可以在运行时查询的信息，并且存在是因为它是基础实现的有用的泄漏抽象。

我能够实际使用“类型”的唯一方法是为我的变量“打标记”，如复合术语number(1)、number(pi)、operator(+)、date(2015, 1, 8)等。然后，我可以放置变量，编写确定性或半确定性谓词，在一周后查看代码时理解我的代码意图....

因此，自由变量和整数只是术语；主要是因为，正如您非常聪明地指出的那样，自由变量可以成为整数、原子或复合术语。您可以使用协同处理确保自由变量稍后只能成为某种“类型”的术语，但从实用角度来看，这仍然不如使用复合术语。

我很可能在混淆非常不同的问题；老实说，我对Prolog的经验极为有限。我只是阅读我正在使用的实现的文档，并尝试找到最好的方法来利用它。

- user1812457

---

must_be/2有很多根本不是类型的“类型”。 - false

@false 是的；我故意将类型“未指定”，以便用户可以根据需要添加临时类型。Prolog中的类型测试并没有完全给Prolog带来类型系统（对吧？不太确定）。用throw(error, ...)替换must_be是否更接近您所需的内容？ - user1812457

或者说：从用户的角度来看。你想要在integer(X)的位置上写has_type(integer,X)吗？ - false

@false 是的。由于在术语标准顺序中自由变量和整数有定义的顺序，这是不可避免的。是否有任何意义将自由变量与整数进行比较是另一个问题。（不，我认为没有意义） - user1812457

@false 是的，我一定是误解了什么。如果两个对象有一个定义好的（严格）排序，那么它们就处于同一个域中。如果你能按照顺序查看两个对象 a 和 b，并确定哪一个是这两个对象中的“最小值”（如果它们在排序方面相同，则 a 应该是最小值），那么显然它们共享一个“类型”。从这里开始，唯一明智的方法（我愚蠢地认为）要么是：1）接受 integer(X) 是一个属性测试，而不是一个类型；要么2）自由变量和整数不应该被排序。 - user1812457