为什么 `f x = x x` 和 `g x = x x x x x` 有相同的类型

Question

我在玩Rank-N类型并尝试输入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）仍然具有相同的类型。 有人能解释一下这是为什么吗？

- Meowcolm Law

---

forall a b. a -> b 是一个函数，它接受“任何”类型作为参数，并返回“任何”东西，根据调用者的要求。它可以在任何函数可以使用的上下文中使用，因为它可以特化到任何函数类型，但是很难构造出一个实例，除了 undefined 或 unsafeCoerce。 - Silvio Mayolo

Answer 1

重点是x :: a -> b是一个函数，能够提供任何类型的值，无论给定什么参数。这意味着x可以应用于自身，结果可以再次应用于x，如此反复。

至少，这就是它向类型检查器所承诺的。类型检查器并不关心是否存在这样的值，只关心类型是否一致。既不能实际调用f，也不能调用g，因为不存在类型为a -> b的值（忽略底部和unsafeCoerce）。

- chepner

Answer 2

这并不比以下事实更让人惊讶:

m :: (∀ a . a) -> (∀ a . a) -> (Int, Bool)
m p q = (p, q)

具有相同的类型

n :: (∀ a . a) -> (∀ a . a) -> (Int, Bool)
n p q = (q, p)

和你的例子类似，这样做是因为普遍量化的参数可以以许多不同的方式使用，在每种情况下编译器都会选择适当的类型并强制 x 作为该类型。

这实际上是一种相当牵强的情况，因为像 ∀ a . a 或 ∀ a b . a->b 这样的类型是无法被 inhabit（除了 ⊥），所以你永远不会真正使用带有这种参数的 RankN 函数；实际上，你也不会写它！

实用的 RankN 函数通常在它们的参数中施加一些额外的结构或类型类约束，比如

foo :: (∀ a . [a] -> [a]) -> ...

或者

qua :: (∀ n . Num n => Int -> n -> n) -> ...

- leftaroundabout

Answer 3

一个更简单的例子

每当我们使用具有多态类型（例如您的 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来表示特定类型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 的选择是完全任意的，我们可以在那里使用任何其他类型。我们甚至可以为每个 x 使用不同的 A 和 B，只要第一个 x 被适当地实例化即可！）

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

- chi