What benefit does types bring in logic programming languages like Mercury?

Question

I've starting looking at the Mercury language, which seems very interesting. I'm a new to logic programming, but pretty experienced with functional programming in Scala and Haskell. One thing I've been pondering is why you need types in logic programming when you already have predicates which should be at least as expressive as types.

For example, what benefit is there to using types in the following snippet (taken from the Mercury tutorial):

:- 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
  ).

compared to writing it using only predicates:

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
  ).

Feel free to point to introductory material which covers this topic.

Edit: I probably was a bit unclear in the formulation of the question. I actually started looking at Mercury after looking into dependent typing languages like Idris, and the same way that values can be used in types in dependent typing, the same way predicates could be used at compilation time to verify the correctness of logic programs. I can see a benefit of using types for compile time performance reasons if the program takes a long time to evaluate (but only if the types are less complex than the "implementation" which is not necessarily the case when talking about dependent typing). My question is if there are other benefits to using types besides compile time performance.

Answer 1

One direct benefit compared to your alternative is that declarations like

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

can be put in the interface to a module separately from the clause. This way, users of the module get constructive, compiler-verified information about the fib predicate, without being exposed to the implementation details.

More generally, Mercury's type system is statically decidable. This means that it is strictly less expressive than using predicates, but the benefit is that the author of the code knows exactly which errors will be caught at compile time. Users can of course still add run time checks using predicates, to cover cases that the type system is unable to catch.

Mercury supports type inference, so dependent types would hit the same problem as predicates with respect to static checking. See this answer for information and further links.