8

我开始研究 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 的，就像在依赖类型中可以在类型中使用值一样，也可以在编译时使用谓词来验证逻辑程序的正确性。如果程序需要很长时间来评估，我可以看到出于编译时性能原因使用类型的好处（但前提是类型不如“实现”复杂，在谈论依赖类型时不一定是这种情况）。我的问题是除了编译时性能之外，使用类型是否还有其他好处。

4

1 回答 1

4

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

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

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

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

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

于 2014-10-05T10:23:31.023 回答