haskell - 当省略 "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

为了清楚起见，添加了括号:

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

在本例中，表达式之前带有 forall 关键字的版本似乎只是为了方便起见。

我说得对吗？

Answer 1

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)