从量化中推导等级

Question

给出以下代码(来自Yoneda引理解释)：

{-# LANGUAGE RankNTypes #-}

check1 :: a -> (forall b . (a -> b) -> b)
check1 a f = f a

uncheck1 :: (forall b . (a -> b) -> b) -> a
uncheck1 t = t id

forall对check1的量化似乎是rank-1，这一点在ghci中得到了证实

$ :t check1
check1 :: a -> (a -> b) -> b
$ :t uncheck1
uncheck1 :: (forall b. (a -> b) -> b) -> a

我不明白为什么check1有rank-1类型签名，而uncheck1仍然保持rank-2类型签名。我将check1的类型签名读为“对于所有类型的b，接受a类型的函数到b ( a是固定的)，并返回一个b类型的值”。这使我相信，用户不允许预先选择b类型(与a类型不同)，因此，类型应该是rank-2。这里似乎有一些细微之处，当我试图了解是否应该将一个显式forall签名理解为级别1或更高级别时，我肯定会错过。

Update:虽然我已经接受了下面的答案，但在看来，来自伦纳特·奥古斯松的这个电子邮件的解释在capital lambda方面是非常清晰和直观的--它消除了调用者的困惑，并清楚地展示了如何进行类型级别的lambda来解释forall。

Answer 1

碰巧，我们可以在forall在check1中浮动，因为它在箭头的右边。

 check1 :: a -> (forall b. (a -> b) -> b)
 check1 :: forall b. a -> (a -> b) -> b

对此的直觉，在uncheck1中，谁能选择b是什么？肯定不是调用者，因为该函数必须适用于所有b。

在check1中，调用者确实可以选择b，因为我们必须返回一个适用于所有b的函数。我们将函数返回给他们，这样他们就可以将其专门化到他们选择的任何地方。因为调用者可以选择任何方式，所以这完全等同于

check1 :: a -> (a -> b) -> b

HaskellWiki页面将讨论这一点。