유형이 수성과 같은 논리 프로그래밍 언어를 가져올 때 어떤 이점이 있습니까?

Question

머큐리 언어를 살펴보기 시작했습니다. 매우 흥미로운 것 같습니다. 나는 논리 프로그래밍에 익숙하지 않지만 스칼라와 하스켈에서 함수형 프로그래밍에 익숙하다. 내가 숙고 해 왔던 한 가지 이유는 적어도 유형처럼 표현력이 있어야하는 술어가 이미있을 때 논리 프로그래밍에서 유형이 필요한 이유입니다.

예를 들어

, 다음 (머큐리 튜토리얼에서 가져온) 코드에서 유형을 사용하여 무슨 이득이 : 만 사용하여 쓰기에 비해

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

하여 주시기 바랍니다 이 주제를 다루는 입문 자료를 가리 키기 위해

편집 : 아마도 질문의 공식에서 조금 명확하지 않았을 것입니다. 필자는 실제로 Idris와 같은 종속 형 타이핑 언어를 살펴본 후 머큐리를 살펴보기 시작했으며, 종속 형 타이프에서 값을 사용할 수있는 것과 같은 방식으로 컴파일 타임에 논리 프로그램의 정확성을 확인하는 데 사용되는 술어와 동일한 방법을 사용했습니다. 프로그램이 평가하는 데 오랜 시간이 걸리는 경우 컴파일 타임 성능상의 이유로 유형을 사용하는 이점을 볼 수 있습니다 (그러나 유형이 종속 유형에 대해 말할 때 반드시 필요한 것은 아닌 "구현"보다 덜 복잡 할 때만). 내 질문은 컴파일 타임 성능 외에도 형식 사용에 다른 이점이 있는지 여부입니다. 당신의 대안에 비해

Answer 1

한 직접적인 혜택을 선언

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

등이 절에서 별도로 모듈 인터페이스에 넣어 될 수 있다는 것이다. 이 방법을 사용하면 모듈 사용자가 구현 세부 사항에 노출되지 않고 fib 술어에 대한 건설적이고 컴파일러 확인 된 정보를 얻습니다.

더 일반적으로 수성 유형 시스템은 정적으로 결정 가능합니다. 이는 술어를 사용하는 것보다 표현력이 덜 표현된다는 것을 의미하지만 코드 제작자는 컴파일 타임에 어떤 오류가 발견되는지 정확하게 알고 있다는 이점이 있습니다. 물론 사용자는 유형 시스템이 포착 할 수없는 경우를 다루기 위해 술어를 사용하여 런타임 검사를 추가 할 수 있습니다.

머큐리는 유형 유추를 지원하므로 종속 유형은 정적 검사와 관련하여 술어와 동일한 문제를 발생시킵니다. 정보 및 추가 링크는 this answer을 참조하십시오.