lambda-calculus - 无法理解 F-omega 术语

Question

我正在阅读一篇关于 F _ω的论文，无法理解这句话背后的原因：

类型 (∀γ:*.F γ → β) 的类型项表明 F 是一个始终返回 β 的常数函数。

我猜“F γ → β”是类型项，即箭头类型。这个箭头类型是一个函数的类型，它接受一个由类型应用程序“F γ”计算的类型的参数，并返回一个类型为 β 的值。

如果是这种情况，为什么 F 应该是一个总是返回 β 的常量（类型）函数？它不能是任意类型的函数，比如返回 α 并且仍然满足类型检查器的函数吗？

谢谢你的时间。

Answer 1

回答我自己的问题。

我认为原因是参数化。

如果 'F γ' 可以返回任何类型，例如 α，则函数（其类型由 ∀ 类型传达）将具有 α → β 的类型。

参数性规定这个多态函数的所有实例都应该具有相同的行为，这只有在它是恒等函数时才有可能，即类型为 β → β，因此暗示“F γ”总是返回 β。