aut*_*hir 7 polymorphism ocaml ml sml parametric-polymorphism
Benjamin C. Pierce 在其类型和编程语言一书的第23.8节中写道:
系统F的另一个充分研究的限制是由Leivant(1983)引入的rank-2多态性 [...].当类型被绘制为树时,如果没有从其根到∀量词的路径传递到2个或更多箭头的左侧,则称类型为等级2.[...]在rank-2系统中,所有类型都被限制为等级2.这个系统比prenex(ML)片段稍强一些,因为它可以为更多无类型的lambda术语分配类型.
Kfoury和Tiuryn(1990)证明了系统F的秩-2片段的类型重建的复杂性与ML的相同(即,DExptime-complete).Kfoury和Wells(1999)给出了秩2系统的第一个正确的类型重建算法,并且表明系统F的等级3和更高的类型重建是不可判定的.
因此,知道秩-2多态的类型推断是可判定的,并且自1999年以来就已知算法.Haskell支持其RankNTypes语言扩展,但它支持rank-n多态.
哪些语言(如果有的话)实现了rank-2参数多态而不是System F？
由于类型推断是可判定的并且没有最差的复杂性,为什么既没有SML也没有OCaml扩展多态性到-2级？
为什么我们没有在野外看到和阅读更多关于rank-2多态性的信息？