作用域类型变量需要显式的 foralls。为什么？

Question

如果你想使用 GHC 的lexically scoped type variables，你也必须使用explicit universal quantification。也就是说，您必须在函数的类型签名中添加 forall 声明：

{-# LANGUAGE ExplicitForAll, ScopedTypeVariables #-}

f :: forall a . [a] -> [a]      -- The `forall` is required here ...
f (x:xs) = xs ++ [x :: a]       -- ... to relate this `a` to the ones above.

这实际上与量化有关吗，或者扩展编写者只是将forall 关键字用作新的更广泛范围适用的方便标记？

换句话说，为什么我们不能像往常一样省略forall？函数体内注解中的类型变量指的是函数签名中的同名变量，这不是很清楚吗？还是打字会有问题或模棱两可？

Answer 1

是的，量词是有意义的，是类型有意义所必需的。

首先请注意，在 Haskell 中确实没有“未量化”类型签名之类的东西。没有forall 的签名实际上是隐式量化的。这段代码...

f :: [a] -> [a]                         -- No `forall` here ...
f (x:xs) = xs ++ [x :: a]               -- ... or here.

...真正的意思是：

f :: forall a . [a] -> [a]              -- With a `forall` here ...
f (x:xs) = xs ++ [x :: forall a . a]    -- ... and another one here.

所以让我们弄清楚这句话是什么意思。重要的是要注意 f 和 x 的签名中名为 a 的类型变量由 separate 量词绑定。这意味着它们是不同的变量，尽管它们共享一个名称。所以上面的代码等价于：

f :: forall a . [a] -> [a]
f (x:xs) = xs ++ [x :: forall b . b]    -- I've changed `a` to `b`

通过区分名称，现在不仅f 和x 的签名中的类型变量是不相关的，而且x 的签名声称x 可以有任何 类型。但这是不可能的，因为当 f 应用于参数时，x 必须将特定类型绑定到 a。事实上，类型检查器会拒绝此代码。

另一方面，f 的签名中只有一个 forall ...

f :: forall a . [a] -> [a]              -- A `forall` here ...
f (x:xs) = xs ++ [x :: a]               -- ... but not here.

...x上的签名中的a是由f的类型签名开头的量词绑定的，所以这个a代表的类型和变量所代表的类型相同在f 的签名中称为a。