Какую пользу приносят типы в языках логического программирования, таких как Mercury?

Question

Я начал смотреть на язык Меркурия, который кажется очень интересным. Я новичок в логическом программировании, но довольно опытный в функциональном программировании в 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
  ).

Не стесняйтесь указывать на вводный материал, который охватывает эту тему.

Редактировать: я, вероятно, был немного неясен в формулировке вопроса. На самом деле я начал смотреть на Mercury после изучения зависимых языков типизации, таких как Idris, и того же способа, которым значения могут использоваться в типах в зависимой типизации, точно так же, как предикаты могут использоваться во время компиляции для проверки правильности логических программ. Я вижу преимущество использования типов по причинам производительности во время компиляции, если программе требуется много времени для оценки (но только если типы являются менее сложными, чем "реализация", что не всегда имеет место, когда речь идет о зависимой типизации). Мой вопрос заключается в том, есть ли другие преимущества использования типов помимо производительности времени компиляции.

Answer 1

Одно прямое преимущество по сравнению с вашей альтернативой заключается в том, что такие объявления, как

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

может быть вставлен в интерфейс к модулю отдельно от пункта. Таким образом, пользователи модуля получают конструктивную, проверенную компилятором информацию о fib предикат, не подвергаясь деталям реализации.

В целом, система типов Меркурия статически разрешима. Это означает, что он строго менее выразителен, чем использование предикатов, но преимущество заключается в том, что автор кода точно знает, какие ошибки будут обнаружены во время компиляции. Конечно, пользователи могут добавлять проверки во время выполнения с использованием предикатов, чтобы охватить случаи, которые система типов не может отловить.

Mercury поддерживает вывод типов, поэтому зависимые типы сталкиваются с той же проблемой, что и предикаты в отношении статической проверки. Смотрите этот ответ для информации и дальнейших ссылок.