省略"forall"时,它们是否真的自动插入语句之前？

Question

forall如果没有指定,很多文章和书籍都会在声明之前明确添加.例如

check :: (forall a. [a] -> Int) -> [b] -> [c] -> Bool

实际上是

check :: forall b. forall c. (forall a. [a] -> Int) -> [b] -> [c] -> Bool

我有一些问题因为Haskell使用currying我会想象最终的签名看起来像:

check :: (forall a. [a] -> Int) -> forall b. [b] -> forall c. [c] -> Bool

为了清晰起见,添加了parens:

check :: (forall a. [a] -> Int) -> (forall b. [b] -> (forall c. [c] -> Bool))

在这种情况下,forall表达式之前带有关键字的版本似乎只是方便的快捷方式.

我对吗？

Answer 1

实际上,forall a. (T -> U a)相当于T -> (forall a. U a).所以你和文章都是正确的.人们使用前者的原因在于它更明显地表明这是一种排名类型.

Answer 2

Haskell的优点在于,您可以通过传递-ddump-simpl给编译器来实际查看使用显式量词的中间语言.正如Tarmil指出的那样,在System Fc重新排列中,此函数中的外部通用量词在语义上是相同的.

-- surface language
check :: (forall a. [a] -> Int) -> [b] -> [c] -> Bool
check = undefined

app1 = check undefined
app2 = check undefined undefined
app3 = check undefined undefined undefined

翻译为:

-- core language
check :: forall b c. (forall a. [a] -> Int) -> [b] -> [c] -> Bool
check = \ (@ b) (@ c) -> (undefined)

app1 :: forall b c. [b] -> [c] -> Bool
app1 = \ (@ b) (@ c) -> check (\ (@ a) -> undefined)

app2 :: forall c. [c] -> Bool
app2 = \ (@ c) -> check (\ (@ a) -> undefined) (undefined)

app3 :: Bool
app3 = check (\ (@ a) -> undefined) (undefined) (undefined)