lambda - 这些多态类型之间有什么区别？

Question

在 System F 中，以下 3 种类型有什么区别：

在此处以文本形式转载：

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

第二个比第一个更通用吗？

Answer 1

取决于forall量词绑定的紧密程度。让我们假设它绑定在下一个终端表达式（变量或()-block）上。

第一个将成为(X0 -> X0) -> (X0 -> X0)whereX0是一个新的类型变量。

第二个将成为新鲜的(X0 -> X0) -> forall X1. (X1 -> X1)地方。X0X1

第三个(bot -> X) -> (bot -> X)是X旧的绑定和机器人是无人居住的地方forall X. X。