スコープタイプの変数には明示的な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キーワードをcooptんでした新しい、より広いスコープが適用されますか？

つまり、いつものようにforallを除外することはできませんか？関数本体内のアノテーションの型変数は、関数シグネチャ内の同じ名前の変数を参照していることは明確ではないでしょうか？または、タイピングが何らかの形で問題になるかあいまいになるか？

Answer 1

はい、量指定子は意味があり、型が意味を成すために必要です。

まず、ハスケルには "非定量化"型署名というものはありません。 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ができることanyタイプがあります。しかし、これは不可能です。xは、fが引数に適用されたときに、特定の型がaにバインドされている必要があるためです。実際には、型チェッカーはこのコードを拒否します。 f ...

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

のシグネチャで単一forallで... xの署名でaがf年代の初めに数量詞に拘束される一方

、したがって、aはの署名にaという変数で表される型と同じ型を表します。