haskell - 从 forall 量化中推导出排名

Question

鉴于以下代码(来自 Yoneda Lemma explanation ):

{-# 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 级或更高级别。

更新:
虽然我已经接受了下面的答案， this email explanation来自 Lennart Augustsson 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页面讨论了这一点。