高等级多态性中"秩"的起源是什么？

Question

我正在寻找类似于更高类型多态性的解释,其中一种类型只是一组谓词.

Answer 1

一个类型的等级描述了通用量词出现逆转的深度(Kfoury&Tiuryn,1992):

Monotypes ?, ?(0) ::= a | ?1 ? ?2
Polytypes ?(n+1) ::= ? n | ? n ? ?(n+1) | ?a.?(n+1)

这里有些例子:

Int ? Int Rank 0
?a.a ? a Rank 1
Int ? (?a.a ? a) Rank 1
(?a.a ? a) ? Int Rank 2