类型给Mercury这样的逻辑编程语言带来了什么好处

Question

我已经开始研究Mercury语言，它看起来非常有趣。我是逻辑编程的新手，但在Scala和Haskell的函数编程方面经验丰富。我一直在思考的一件事是，当你已经有了谓词时，为什么你在逻辑编程中需要类型，这些谓词至少应该和类型一样具有表达能力。

例如，在以下片段中使用类型有什么好处（取自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支持类型推断，因此在静态检查方面，依赖类型将遇到与谓词相同的问题。有关信息和进一步的链接，请参阅此答案。