高ランク多型における「ランク」の起源は何ですか？

Question

私は高級多型と同様の説明を探しています。種類は単に述語型の集合です。

Answer 1

タイプのランクが普遍数量詞がcontravariantly（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 

https://functionalprogramming.slack.com/archives/C0432GV99/p1509647117000276