范围类型变量需要明确的foralls.为什么？

Question

如果要使用GHC的词法范围变量,则还必须使用显式通用量化.也就是说,您必须向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中确实没有"未量化"类型签名.没有a的签名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签名for f和for x中命名的类型变量由单独的量词绑定.这意味着它们是不同的变量,尽管共享一个名称.所以上面的代码相当于:

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

由于名称有所区别,现在不仅清楚签名中的类型变量f和x不相关,而且可以是任何类型的x声明的签名.但是,这是不可能的,因为必须具有绑定到特定类型时被施加到一个参数.事实上,类型检查器会拒绝此代码.xxaf

另一方面,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的签名.