作用域类型变量需要显式作用。为什么？ [英] Scoped type variables require explicit foralls. Why?

问题描述

如果您想使用GHC的词汇范围类型变量，您还必须使用显式通用量化。也就是说，你必须添加 forall 声明到你的函数的类型签名中：

  { - ＃LANGUAGE ExplicitForAll，ScopedTypeVariables＃ - } 
 
f :: forall a。 [a]  - > [a]  - 这里需要'forall'... 
 f（x：xs）= xs ++ [x :: a]  -  ...将这个'a'与上面的那个关联起来。 
  

这实际上是否与量化有关，还是扩展编写者只是共同使用 forall 关键字作为新的更广泛的范围适用范围的方便标记？

换句话说，为什么我们不能离开像往常一样从 forall 出？难道不清​​楚函数体内的注释中的类型变量是指函数签名中的同名变量吗？或者这种打字会出现问题或模糊不清？

解析方案

是的，量词是有意义的，并且这些类型是有意义的。

首先请注意，Haskell中确实没有像未量化类型签名那样的东西。没有 forall 的签名实际上是隐式量化的。此代码...

  f :: [a]  - > [a]  - 这里没有`forall` ... 
 f（x：xs）= xs ++ [x :: a]  -  ...或者这里。 
  

...真的意味着这个：

  f :: forall a。 [a]  - > [a]  - 在这里用'forall'... 
 f（x：xs）= xs ++ [x :: forall a。一个]  -  ...和另一个在这里。 
  

让我们来看看这是什么意思。重要的是要注意 f 和 a > x 被单独量词限制。这意味着它们是不同的变量，尽管共享一个名称。所以上面的代码就相当于这个：

  f :: forall a。 [a]  - > [a] 
 f（x：xs）= xs ++ [x :: forall b。 b]  - 我把`a`改成了`b` 
  

现在不仅要清楚 f 和 x 的签名中的类型变量是不相关的，而且 x 声称 x 可以有任何类型。但是这是不可能的，因为当 f 时， x 必须具有绑定到 a / code>应用于参数。实际上，类型检查器会拒绝此代码。



另一方面，签名中的单个 forall 对于 f ...

  f :: forall a。 [a]  - > [a]  - 'forall`在这里... 
 f（x：xs）= xs ++ [x :: a]  -  ...但不在这里。 
  

...签名中的 a x 在 f 的类型签名开始处由量词绑定，所以 表示与 f 中由 a 变量表示的类型相同的类型。的签名。

If you want to use GHC's lexically scoped type variables, you also have to use explicit universal quantification. That is, you have to add forall declarations to your functions' type signatures:

{-# 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.

Does this actually have anything to do with quantification, or did the extension writers just coopt the forall keyword as a convenient marker for where the new, wider scoping applies?

In other words, why can't we leave out the forall as usual? Wouldn't it be clear that type variables in annotations within the function body refer to variables of the same name in the function signature? Or would the typing be somehow problematic or ambiguous?

解决方案

Yes, the quantifier is meaningful and is required for the types to make sense.

First note that there's really no such thing as an "unquantified" type signature in Haskell. Signatures without a forall are really implicitly quantified. This code ...

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

... really means this:

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

So let's figure out what this says. The important thing is to notice that the type variables named a in the signatures for f and for x are bound by separate quantifiers. This means that they are different variables, despite sharing a name. So the above code is equivalent to this:

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

With the names differentiated, it's now clear not only that the type variables in the signatures for f and x are unrelated, but that the signature for x claims that x can have any type. But this is impossible, since x must have the particular type bound to a when f is applied to an argument. And indeed the type-checker rejects this code.

On the other hand, with a single forall in the signature for f ...

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

... the a in the signature on x is bound by the quantifier at the beginning of f's type signature, so this a represents the same type as the type represented by the variables called a in f's signature.

这篇关于作用域类型变量需要显式作用。为什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！