我已经玩了几个小时的swi-prolog了，我试图模仿一个简单的多态类型系统，却陷入了死胡同。所以，在我花了太多的时间试图摆脱困境之前，让我问你们一个如下的问题：假设，我有一个名为 "关系 "的声明，名为 top，这标志着它的单个 arg 是一个类型。
top(nat). % naturals
top(list(T, _)) :- top(T). % polymorphic lists
我还为Nats提供了类似Peano的经典定义，为Lists提供了一些合理的定义。
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) 在prolog中。是不是因为prolog是基于一阶逻辑，在谓词上没有量化？如果是这样，有什么变通办法吗？
所以，我最终得到了这样的代码：
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 - 类型的一种。
谢谢你们，加油。
你的目标 call(T, TT, A, _) 想叫 nat 有三个参数，但没有 nat/3 谓词。你对类型的种类进行了检查，但它们来得太晚了。你的 arity 应运而生 之前 相应 call. 然而，即使如此，在第二个分支中，你也要检查一个类型的 T 性质为1的，即 list，但没有办法调用 list/2 有三个参数...
你的整个模型有点混乱，因为你试图将所有的东西--包括值和类型--都建模为Prolog谓词。事实上，两者都不应该是谓词。甚至连类型都不是! 这将 似乎 类型作为谓词是个不错的主意，因为这将允许像这样的查询。
?- 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.