algorithm - 算法 W(或 Haskell)中的函数参数不是多态的吗？

Question

我正在实现 Algorithm W对于一种玩具语言。我遇到了一个我想象会键入检查的案例，但没有。我在 Haskell 中尝试过同样的方法，令我惊讶的是它也没有在那里工作。

> (\id -> id id 'a') (\x -> x)
Couldn't match type ‘Char -> t’ with ‘Char’
Expected type: Char -> t
Actual type: (Char -> t) -> Char -> t

我假设 id将是多态的，但似乎不是。请注意，如果 id，则此示例有效。使用 let 定义而不是作为参数传递:

let id x = x in id id 'a'
'a'
:: Char

在查看算法 W 的推理规则时，这是有道理的，因为它具有 let 表达式的泛化规则。
但我想知道这是否有任何原因？函数参数不能被泛化以便可以多态使用吗？

Answer 1

泛化 lambda 绑定(bind)变量的问题在于它需要更高等级的多态性。举个例子:

(\id -> id id 'a')

如果 id 的类型这里是 forall a. a -> a , 那么整个 lambda 表达式的类型必须是 (forall a. a -> a) -> Char ，这是等级 2 的类型。
除了这个技术点之外，还有一个论点是更高等级的类型非常罕见，因此与其推断非常罕见的类型，不如说用户更可能犯了错误。