类型对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 的类型系统是静态可判定的。这意味着严格来说它的表达能力不如使用谓词，但好处是代码的作者确切地知道在编译时将捕获哪些错误。当然，用户仍然可以使用谓词添加运行时检查，以覆盖类型系统无法捕获的情况。

Mercury 支持类型推断，因此依赖类型会遇到与静态检查方面的谓词相同的问题。请参阅此答案以获取信息和进一步的链接。