Jakie korzyści przynoszą typy w logicznych językach programowania, takich jak Mercury?

Question

Zaczynam od patrzenia na język Mercury, co wydaje się bardzo interesujące. Jestem nowy w programowaniu logiki, ale dość doświadczony w programowaniu funkcjonalnym w Scali i Haskell. Jedną z rzeczy, nad którą się zastanawiałem, jest to, dlaczego potrzebujesz typów w programowaniu logicznym, gdy masz już predykaty, które powinny być co najmniej tak ekspresyjne jak typy.

Na przykład, jakie korzyści ma do korzystania z typów w następującym fragmencie (zaczerpnięte z tutorialu rtęć):

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

porównaniu do pisania przy użyciu tylko predykaty:

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

Zapraszam wskazać materiał wprowadzający, który obejmuje ten temat.

Edycja: Prawdopodobnie nie było jasne w formułowaniu pytania. Właściwie zacząłem spoglądać na Merkurego po zapoznaniu się z zależnymi językami pisania, takimi jak Idris, i tym samym sposobem, w jaki wartości mogą być używane w typach w zależnym typowaniu, w ten sam sposób, w jaki sposób predykaty mogą być używane w czasie kompilacji do sprawdzenia poprawności programów logicznych. Widzę korzyści wynikające z używania typów dla celów związanych z wydajnością w czasie kompilacji, jeśli ocena zajmuje dużo czasu (ale tylko wtedy, gdy typy są mniej złożone niż "implementacja", co niekoniecznie musi się zdarzyć, gdy mówimy o pisaniu zależnym). Moje pytanie brzmi, czy istnieją inne korzyści z używania typów oprócz czasu kompilacji.

Answer 1

Jeden bezpośrednie korzyści w porównaniu do alternatywnych że deklaracje jak

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

można umieścić w interfejsie do modułu oddzielnie od klauzuli. W ten sposób użytkownicy modułu otrzymują konstruktywne, zweryfikowane przez kompilator informacje o predykacie fib, bez narażania się na szczegóły implementacji.

Bardziej ogólnie, system typu Mercury jest statycznie rozstrzygalny. Oznacza to, że jest to mniej ekspresywne niż używanie predykatów, ale korzyścią jest to, że autor kodu dokładnie wie, które błędy zostaną przechwycone podczas kompilacji. Użytkownicy mogą oczywiście nadal dodawać kontrole czasu pracy za pomocą predykatów, aby uwzględnić przypadki, których system typów nie jest w stanie przechwycić.

Rtęć obsługuje wnioskowanie o typie, więc typy zależne miałyby taki sam problem jak predykaty w odniesieniu do sprawdzania statycznego. Aby uzyskać więcej informacji i dalsze linki, patrz this answer.