types - Mercury のような論理プログラミング言語に型はどのような利点をもたらしますか?

Question

Mercury 言語を調べ始めましたが、これは非常に興味深いと思われます。私はロジック プログラミングは初めてですが、Scala と Haskell での関数型プログラミングにはかなりの経験があります。私が考えていることの 1 つは、少なくとも型と同じくらい表現力のある述語が既にあるのに、なぜ論理プログラミングで型が必要なのかということです。

たとえば、次のスニペットで型を使用する利点は何ですか (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 に注目し始めました。依存型型付けの型で値を使用できるのと同じ方法で、論理プログラムの正確性を検証するためにコンパイル時に述語を使用できるのと同じ方法です。プログラムの評価に長い時間がかかる場合、コンパイル時のパフォーマンス上の理由から型を使用する利点が見られます (ただし、依存型の型付けについて話すときは必ずしもそうではない「実装」よりも型が複雑でない場合のみ)。私の質問は、コンパイル時のパフォーマンス以外に型を使用する利点があるかどうかです。