這些多態類型之間的區別是什麼？

Question

在系統F，就是以下3種類型之間的差異：

轉載的文字在這裏：

∀X.((X → X) → (X → X)) 
∀X.((X → X) → ∀X.(X → X)) 
((∀X.X → X) → (∀X.X → X)) 

是第二個更普遍比第一？

Answer 1

取決於量詞結合的程度。讓我們假設它綁定到下一個終端表達式（變量或()-block）。

第一個將變成(X0 -> X0) -> (X0 -> X0)其中X0是一個新鮮的類型變量。

第二個將變成(X0 -> X0) -> forall X1. (X1 -> X1)其中X0和X1是新鮮的。

第三個 - (bot -> X) -> (bot -> X)其中X是舊綁定，bot是無人居住的forall X. X。