Prolog:简单多态类型模型


初始员额

我已经玩了几个小时的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.

给TA打赏
共{{data.count}}人
人已打赏
未分类

如何设置报表仪表盘的数据库

2022-9-13 14:07:39

未分类

python: 独立移动张量中的每个矩阵。

2022-9-13 14:07:41

0 条回复 A文章作者 M管理员
    暂无讨论,说说你的看法吧
个人中心
购物车
优惠劵
今日签到
有新私信 私信列表
搜索