我在玩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
)仍然具有相同的类型。
有人能解释一下这是为什么吗?
我在玩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
)仍然具有相同的类型。
有人能解释一下这是为什么吗?
x :: a -> b
是一个函数,能够提供任何类型的值,无论给定什么参数。这意味着x
可以应用于自身,结果可以再次应用于x
,如此反复。f
,也不能调用g
,因为不存在类型为a -> b
的值(忽略底部和unsafeCoerce
)。这并不比以下事实更让人惊讶:
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) -> ...
每当我们使用具有多态类型(例如您的 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 ...
是一个更长的序列,也显然是可能的。
forall a b. a -> b
是一个函数,它接受“任何”类型作为参数,并返回“任何”东西,根据调用者的要求。它可以在任何函数可以使用的上下文中使用,因为它可以特化到任何函数类型,但是很难构造出一个实例,除了undefined
或unsafeCoerce
。 - Silvio Mayolo