lambda - これらのポリモーフィック型の違いはどれですか?

Question

システム F では、次の 3 つのタイプの違いは何ですか。

ここにテキストで再現：

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

2番目のものは最初のものよりも一般的ですか?

Answer 1

forall量指定子のバインドの強さに依存します。()次の端末式 (変数または-block)にバインドすると仮定しましょう。

最初は(X0 -> X0) -> (X0 -> X0)where X0is a fresh type variable になります。

(X0 -> X0) -> forall X1. (X1 -> X1)2つ目はどこX0になるのかX1新鮮です。

3 番目の(bot -> X) -> (bot -> X)場所Xは古いバインディングで、ボットは無人forall X. Xです。