Пролог: модель простой полиморф c тип

Question

Начальный пост

Я играю со swi-prolog уже несколько часов и зашел в тупик, пытаясь имитировать c простую систему типа polymorphi c. Итак, прежде чем я потратил много времени, пытаясь выбраться, позвольте мне задать вам, ребята, следующий вопрос: Скажем, я объявил отношение с именем top, которое помечает один аргумент как тип.

top(nat).                  % naturals
top(list(T, _)) :- top(T). % polymorphic lists 

и у меня также есть classi c Peano-подобное определение для Nats и несколько разумное определение для списков:

nat(zero).
nat(s(A)) :- nat(A).  

list(T, nil) :- top(T).
list(T, cons(T, _, _)) :- top(T)

на данный момент, единственное, что осталось, это реализация для конструктор cons. Самое простое определение, которое приходит мне в голову:

cons(T, A, B) :- top(T), list(T, B), T(A).

Но, оказывается, вы не можете иметь T(A) в прологе. Это потому, что пролог основан на логиках первого порядка c, где количественное определение предикатов недоступно? Если да, есть ли обходной путь?

Обновление:

Итак, я получил такой код:

top.

type(top, top).
type(top, nat).
type(top, container(T)) :- type(top, T).
type(top, either(A, B)) :- type(top, A), type(top, B).

type(nat, zero).
type(nat, s(A)) :- type(nat, A).

type(container(T), nil) :- type(top, T).
type(container(T), cons(Head, Tail)) :- 
    type(T, Head),
    type(container(T), Tail).

type(either(A, _), left(V)) :- type(A, V).
type(either(_, B), right(V)) :- type(B, V).

, который позволяет мне создавать контейнеры значений любого типа, включая тип top - тип типов.

Спасибо, ребята, ура.

Answer 1

Ваша цель call(T, TT, A, _) пытается вызвать nat с тремя аргументами, но предиката nat/3 нет. У вас есть чеки на тип, но они приходят слишком поздно: ваш arity чек должен прийти до соответствующего call. Однако, даже тогда, во второй ветви вы проверяете тип T с арностью 1, который будет list, но нет никакого способа вызвать list/2 с тремя аргументами либо ...

Вся ваша модель несколько сбита с толку, потому что вы пытаетесь смоделировать все - и значения, и типы - в соответствии с предикатами Пролога. На самом деле ни один из них не должен быть предикатом. Даже не типы! может показаться хорошей идеей иметь типы в качестве предикатов, так как это будет разрешать такие запросы, как:

?- list(T, cons(0, nil)).
T = nat.

Но не было бы способа спросить "что это за тип cons(0, nil)? ", Это, вероятно, тот тип вопросов, который вы хотели бы задать.

Поэтому вместо этого давайте смоделируем оба значения и их типы как термины, которые связаны отношением типизации, реализованным как Prolog сказуемое. Это очень просто:

value_type(Nat, nat) :-
    nat(Nat).

value_type(nil, list(_A)).
value_type(cons(Head, Tail), list(A)) :-
    value_type(Head, A),
    value_type(Tail, list(A)).

nat(0).
nat(s(A)) :-
    nat(A).

Итак, теперь мы можем задать вопрос сверху: «что это за список` cons (0, nil)? »:

?- value_type(cons(0, nil), list(T)).
T = nat.

Но также теперь мы можем спросить, «какой тип cons(0, nil)?»:

?- value_type(cons(0, nil), T).
T = list(nat).

Это также легко распространить на другие виды значений. Каждый конструктор значений обычно должен добавлять одно определение к определению. Например, мы можем добавить сложение к натуральным числам и функцию length, которая связывает мир списков с миром натуральных чисел:

value_type(X + Y, nat) :-
    value_type(X, nat),
    value_type(Y, nat).

value_type(length(Xs), nat) :-
    value_type(Xs, list(_A)).

Позволяет нам печатать выражения вроде:

?- value_type(length(cons(nil, nil)) + length(nil), Type).
Type = nat.