haskell - 作用域类型变量需要显式 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.

所以让我们弄清楚这句话说的是什么。重要的是要注意名为 a 的类型变量在 f 的签名中和 x由单独的量词绑定(bind)。这意味着尽管它们共享一个名称，但它们是不同的变量。所以上面的代码相当于这样:

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

通过区分名称，现在不仅可以清楚地看出 f 签名中的类型变量和x不相关，但 x 的签名声称x可以有任何类型。但这是不可能的，因为 x必须将特定类型绑定(bind)到 a当f应用于论证。事实上，类型检查器拒绝了此代码。

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

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

...a在 x 的签名中受 f 开头的量词约束的类型签名，所以这个 a表示与名为 a 的变量表示的类型相同的类型在f的签名。