可以将自身作为参数传递的函数类型

Question

深入思考这个计算中的类型，非常深入

id id

从右到左，第一个id有类型

 a -> a

这意味着将第一个作为参数的第二个 id 必须具有类型

(a -> a) -> (a -> a)

类型不匹配！好吧，你可以说 first id 实际上有这个后来的类型，但是这会使 second id 成为类型

((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))

我认为尽管函数可以具有泛型或变量类型，但函数在计算时会绑定到某些类型。在我看来，似乎每次调用都定义了一个 new id 函数。

Answer 1

你是对的。 id 是多态的。 每个 使用都会独立实例化其类型。例如，考虑像id "Hello" ++ show (id 5) 这样的愚蠢的东西。第一次使用时，它是id :: String -> String。在第二次使用中，它是id :: Integer -> Integer（至少具有多态文字的正常默认规则）。通过嵌套对 id 的调用所做的事情是相同的——只是在最内层放入了一些类型变量，而不是具体类型。

不过，这并不意味着实现会发生变化。 id 始终是相同的功能。每次使用时唯一改变的是类型检查器如何处理它。

顺便说一句，这是可以用来使 GHC 的类型检查器崩溃的东西。您已经注意到 id 类型的大小在您将其应用于自身几次时呈指数增长。多做几次，它需要比你的系统更多的内存来表示最外层id的类型。

Answer 2

处理这种情况的正确技术是多态。恒等函数

id x = x

具有类型 ∀α 。 α → α，读作“对于每个类型 α，id 将类型 α 的元素映射到类型 α 的元素”。给应用一个类型

id id

我们争论如下：

• 第一个 id 具有类型 ∀α 。 α → α，
• 第二个id 具有类型 ∀β 。 β → β 其中我们将绑定变量 α 重命名为 β 以避免混淆，
• 如果我们将第一个 id 中的 α 设置为 ∀β 。 β → β 然后我们看到第一个 id 映射类型为 ∀β 的元素。 β → β 到类型 ∀β 的元素。 β → β,
• 因此整个表达式没问题并且具有类型 ∀β 。 β → β，与 ∀α 相同。 α → α。

这并不神秘。延伸阅读：System F.