类型为 Mercury 等逻辑编程语言带来什么好处？

Question

我开始研究 Mercury 语言，这似乎很有趣。我是逻辑编程的新手，但对 Scala 和 Haskell 的函数式编程非常有经验。我一直在思考的一件事是，当您已经拥有至少应该与类型一样具有表达力的谓词时，为什么在逻辑编程中还需要类型。

例如，在以下 sn-p 中使用类型有什么好处（取自 Mercury 教程）：

:- type list(T) ---> [] ; [T | list(T)].

:- pred fib(int::in, int::out) is det.
fib(N, X) :-
  ( if N =< 2
  then X = 1
  else fib(N - 1, A), fib(N - 2, B), X = A + B
  ).

与仅使用谓词编写相比：

list(T, []).
list(T, [H | X]) :- T(H), list(T, X).

int(X) :- .... (builtin predicate)

fib(N, X) :-
  int(N),
  int(X),
  ( if N =< 2
  then X = 1
  else fib(N - 1, A), fib(N - 2, B), X = A + B
  ).

请随意指出涵盖该主题的介绍性材料。

编辑： 我可能在问题的表述上有点不清楚。实际上，我是在研究了 Idris 等依赖类型语言之后才开始研究 Mercury 的，就像在依赖类型中可以在类型中使用值一样，也可以在编译时使用谓词来验证逻辑程序的正确性。如果程序需要很长时间来评估，我可以看到出于编译时性能原因使用类型的好处（但前提是类型不如“实现”复杂，在谈论依赖类型时不一定是这种情况）。我的问题是除了编译时性能之外，使用类型是否还有其他好处。

Answer 1

与您的替代方案相比，一个直接的好处是声明像

:- pred fib(int::in, int::out) is det.

可以与子句分开放在模块的接口中。这样，模块的用户就可以获得关于 fib 谓词的建设性的、经过编译器验证的信息，而无需了解实现细节。

更一般地说，Mercury 的类型系统是静态可判定的。这意味着它比使用谓词严格地表达更少，但好处是代码的作者确切地知道在编译时将捕获哪些错误。用户当然仍然可以使用谓词添加运行时检查，以涵盖类型系统无法捕获的情况。

Mercury 支持类型推断，因此在静态检查方面，依赖类型会遇到与谓词相同的问题。有关信息和更多链接，请参阅this answer。