Welchen Vorteil bringen Typen logische Programmiersprachen wie Mercury?

Question

Ich habe angefangen, die Mercury Sprache zu betrachten, die sehr interessant scheint. Ich bin ein Neuling in der Logikprogrammierung, aber ziemlich erfahren in der funktionalen Programmierung in Scala und Haskell. Eine Sache, über die ich nachgedacht habe, ist, warum Sie Typen in der Logikprogrammierung brauchen, wenn Sie bereits Prädikate haben, die mindestens so ausdrucksstark sein sollten wie Typen.

Zum Beispiel, was Nutzen gibt es Typen im folgenden Ausschnitt (aus den Mercury-Tutorial) zu verwenden:

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

im Vergleich zu schreiben es Prädikate mit nur:

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

Fühlen Sie sich frei auf Einführungsmaterial verweisen, das dieses Thema abdeckt.

Edit: Ich war wahrscheinlich ein bisschen unklar in der Formulierung der Frage. Tatsächlich habe ich angefangen, Mercury zu betrachten, nachdem ich in abhängige Schreibsprachen wie Idris geschaut habe, und genau so, wie Werte in Typen der abhängigen Typisierung verwendet werden können, genauso wie Prädikate zur Kompilierungszeit verwendet werden könnten, um die Korrektheit von Logikprogrammen zu überprüfen. Ich kann einen Vorteil der Verwendung von Typen zur Kompilierzeit Leistungsgründe sehen, wenn das Programm eine lange Zeit für die Auswertung benötigt (aber nur, wenn die Typen weniger komplex sind als die "Implementierung", die nicht unbedingt der Fall ist, wenn man über abhängige Typisierung spricht). Meine Frage ist, ob es neben der Kompilierzeit auch andere Vorteile für die Verwendung von Typen gibt.

Answer 1

Ein direkter Nutzen im Vergleich zu Ihrer Alternative ist, dass Erklärungen wie

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

aus der Klausel gesondert in der Schnittstelle zu einem Modul gestellt werden. Auf diese Weise erhalten die Benutzer des Moduls konstruktive, vom Compiler verifizierte Informationen über das Prädikat , ohne den Details der Implementierung ausgesetzt zu sein.

Allgemeiner, Merkurs Typsystem ist statisch entscheidbar. Dies bedeutet, dass es streng weniger aussagekräftig ist als die Verwendung von Prädikaten, aber der Vorteil besteht darin, dass der Autor des Codes genau weiß, welche Fehler zur Kompilierzeit erfasst werden. Benutzer können natürlich weiterhin Laufzeitprüfungen mit Prädikaten hinzufügen, um Fälle abzudecken, die das Typsystem nicht abfangen kann.

Mercury unterstützt Typinferenz, so dass abhängige Typen das gleiche Problem wie Prädikate in Bezug auf statische Überprüfung haben. Informationen und weitere Links finden Sie unter this answer.