作用域類型變量需要顯式作用。爲什麼？

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的類型變量受限於單獨的量詞。這意味着他們是不同變量，儘管共享一個名字。所以上面的代碼是相同的：

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

提供差異化​​的名字，它現在不僅表明在簽名f和x類型變量是不相關的，但對於x索賠的簽名x能有任何類型。但這是不可能的，因爲x必須將f應用於參數時，必須將具體類型綁定到a。實際上，類型檢查器拒絕這些代碼。

在另一方面，在f簽名單forall ...

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

...的a在x簽名是由量詞在f年代初的約束因此這個a代表與中f的簽名中的變量所代表的類型相同的類型。