Prolog: model simple polymorphic type

Question

Initial post

I've been playing with swi-prolog for a several hours now and I got to dead end trying to mimic a simple polymorphic type system. So, before I have spent way to much time trying to get out, let me ask you guys a following question: Say, I have declared relation named top, that marks it`s single arg as a type.

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

and I also have classic Peano-like definition for Nats and somewhat reasonable definition for Lists:

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

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

at this point, the only thing left is an implementation for 'constructor' cons. The most straightforward definition, that pops in my mind is

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

But, turns out, you cant have T(A) in prolog. Is it because prolog is based on first order logic, where quantification over predicates is not available? If so, is there any workaround?

Update:

So, I ended up with a code like this:

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

which allows me to construct containers of values of any type, including the type top - a type of types.

Thank you guys, cheers.

I don't think CapelliC's answer is what you are after. Is cons(T,A,B) the type-checking predicate? You indeed cannot have T in predicate position because of FOL, but to check A for its type, it has to have its own type label, which must be somewhere in the term structure of A? As an example, Lambda Prolog has a type system but it's "behind the curtains", maybe you need a meta-interpreter? — David Tonhofer
@DavidTonhofer the goal here is not getting a typed version of prolog language, rather I am interested in logical inference in some made up type system. Thanks anyway, please see the update. — hello world

Isabelle Newbie Isabelle Newbie · Accepted Answer · 2020-04-27T19:37:53

Your goal call(T, TT, A, _) is trying to call nat with three arguments, but there is no nat/3 predicate. You have checks on the type's kind, but they come too late: Your arity check should come before the corresponding call. However, even then, in the second branch you're checking for a type T with arity 1, which would be list, but there is no way to call list/2 with three arguments either...

Your whole model is somewhat confused because you are trying to model everything -- both values and types -- as Prolog predicates. In fact neither should be a predicate. Not even types! It would seem like a good idea to have types as predicates, since that would allow queries like:

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

But there would be no way of asking "what is the type of cons(0, nil)?", which is probably the kind of question that you would like to be able to ask.

So instead let's model both values and their types as terms that are connected by a typing relation implemented as a Prolog predicate. This is very simple:

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

So now we can ask the question from above, "what kind of list is `cons(0, nil)?":

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

But also we can now ask, "what is the type of cons(0, nil)?":

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

This is also easy to extend to other kinds of values. Every value constructor should typically add a single clause to the definition. For example, we can add addition on natural numbers, and a length function that connects the world of lists with the world of natural numbers:

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

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

Allowing us to type expressions like:

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

Prolog: model simple polymorphic type

Initial post

Update:

1 Answers