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.

Gausman

Are you saying that run-time type assertions in a logic programming language are somehow a better replacement for static types than run-time type assertions in functional or procedural languages are? – Meggs

No, I was a bit unclear, see my edit of the question. – Gausman

I think what I'm looking for is a language with automated theorem proving like Why3 or Astrée. The downside is that these solutions (like SMT solvers) are limited and/or unpredictable, whereas type systems are robust (but also limited). It seems to be an active research area though, and there is even projects that extend Haskell with SMT solvers. – Gausman

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.

Dougald

Thanks for the reply. Regarding your first argument it seems to me that it would be possible to replace the types with implication in the interface as well (in this case fib(N, X) :- int(N), int(X)). – Gausman

@JesperNordenberg That implication is the wrong way around - you mean to say that if fib(N, X) is true then N and X are integers. But yes, it is possible to do as you suggest. The question is, is it desirable? From a language design point of view, more expressiveness for the author of a module means more complexity for the users of it. – Dougald

Yes, the direction of the implication is interesting. In a functional language fib would have the type (N: Int) -> (X: Int), which means you can give fib any Int and it will always give you an Int back. But it can't give you back an N for every result X, so the proposition should be something like forall N. (int(N) -> exists X. (int(X) & fib(N, X))). Maybe this is how fib(int::in, int::out) is interpreted in the Mercury type system. – Gausman

Yes, that proposition is part of the meaning of is det, another part being that X is unique for each N. In Mercury the modes and determinism provide information in addition to the types. For the purposes of this question, however, modes and determinism provide much the same benefit as types. – Dougald