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

Question

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

例如，在下面的代码片段中使用类型有什么好处(取自水星教程)：

:- 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支持类型推断，因此在静态检查方面，依赖类型将遇到与谓词相同的问题。有关信息和更多链接，请参阅this answer。