为什么 `fx = xx` 和 `gx = xxxxx` 具有相同的类型

Question

我正在玩 Rank-N-type 并尝试输入x x. 但我发现这两个函数可以用相同的方式输入，这是违反直觉的。

f :: (forall a b. a -> b) -> c
f x = x x

g :: (forall a b. a -> b) -> c
g x = x x x x x

我还注意到类似f x = x x ... x x（许多x）的东西仍然具有相同的类型。谁能解释为什么会这样？

Answer 1

关键是这是一个可以提供任何x :: a -> b类型值的函数，无论给出什么参数。这意味着可以应用于自身，并且结果可以再次应用于，依此类推。xx

至少，这就是它向类型检查器承诺的功能。类型检查器不关心是否存在任何此类值，只关心类型是否对齐。实际上， norf都不g能被调用，因为不a -> b存在这样的类型值（忽略bottom 和unsafeCoerce）。

Answer 2

一个更简单的例子

每当我们使用具有多态类型的变量（例如您的x）时，就可以观察到这种现象。恒等函数id也许是最著名的例子。

id :: forall a . a -> a

在这里，所有这些表达式都进行类型检查，并且具有类型Int -> Int：

id :: Int -> Int
id id :: Int -> Int
id id id :: Int -> Int
id id id id :: Int -> Int
...

这怎么可能？好吧，关键在于，每次我们编写时，id我们实际上意味着“a应该从上下文中推断出某种未知类型的恒等函数”。至关重要的是， 的每种用途id都有其自己的a.

我们将其写id @T为 type 上的特定恒等函数T。

写作

id :: Int -> Int

实际上意味着

id @Int :: Int -> Int

这很简单。相反，写

id id :: Int -> Int

实际上意味着

id @(Int -> Int) (id @Int) :: Int -> Int

其中第一个id现在指的是功能空间Int -> Int！而且当然，

id id id :: Int -> Int

方法

(id @((Int -> Int) -> (Int -> Int))) (id @(Int -> Int)) (id @Int) :: Int -> Int

等等。我们没有意识到类型会变得如此混乱，因为 Haskell 为我们推断了这些类型。

具体案例

根据您的具体情况，

g :: (forall a b. a -> b) -> c
g x = x x x x x

我们可以通过多种方式进行类型检查。一种可能的方法是定义A ~ Int, B ~ Bool,T ~ (A -> B)然后推断：

g x = x @T @(T -> T -> T -> c) (x @A @B) (x @A @B) (x @A @B) (x @A @B)

我建议花一些时间来了解所有内容的类型检查。A（此外，我们对和 的选择B是完全任意的，我们可以在那里使用任何其他类型。我们甚至可以为每个使用不同的As 和s ，只要第一个被适当实例化！）Bxx

显然，即使x x x ...序列较长，这样的推断也是可能的。