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

Question

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

haskellghctype-systemsquantifierstype-extension

28

如果您想使用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？在函数体注释中，类型变量引用函数签名中同名变量不是很清楚吗？或者类型检查会出现问题或模棱两可吗？

- pash

1

我在下面提交了自己的答案，但我想知道是否还有其他我没有考虑到的细微之处。... - pash

9

由于Haskell-98没有作用域，只通过forall引入具有作用域的变量是一种妥协方式。这样，当启用ScopedTypeVariables时，旧代码仍然可以运行。（可以说，Haskell应该始终具有作用域类型变量。） - augustss

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- pash · Accepted Answer

是的，量词是有意义的，并且需要使类型合理。

首先请注意，在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的类型变量受到不同的量词约束。这意味着尽管它们共享一个名称，但它们是不同的变量。因此，上述代码等价于以下代码：

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.

在f的类型签名开头的量词约束下，x签名中的a与f签名中称为a的变量表示相同类型。