从forall量化中扣除等级

Question

鉴于下面的代码(来自Yoneda Lemma解释):

{-# 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级或更高级别时,我肯定会发现一些细微差别.

更新: 虽然我已经接受了下面的答案,但我认为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页面讨论这一点.