存在量の数値化はどのタイプでどこで使用できるのかという一般的な考えがあります。しかし、これまでの私の経験から、概念を効果的に使用するために理解する必要がある多くの警告があります。ハスケルの存在量を詳細に数値化する
質問： GHCに存在量の定量化がどのように実装されているかを説明する良いリソースはありますか？私。
私の目的は、GHCが私にスローするエラーメッセージをよりよく理解することです。メッセージは通常、"this type using forall and this other type don't match"という行に沿って何かを言いますが、なぜそうであるかは説明していません。
サイモン・ペイトン・ジョーンズの論文には詳細が記載されていますが、それを理解するには十分な専門知識が必要です。 Haskell型推論がどのように機能するかについての論文を読んでみたい場合は、実在型と他のいくつかの機能を組み合わせた一般化された代数データ型（GADT）を読むべきです。私は、http://research.microsoft.com/en-us/people/simonpj/の論文のリストにある「GADTの完全かつ決定可能な型推論」を提案します。
実際の定量化は、実際に普遍的な定量化のように多く機能します。ここでは、2つの間の平行線を強調する例を示します。関数useExisは役に立ちませんが、それでも有効なコードです。まず
data Univ a = Univ a
data Exis = forall a. Exis a
toUniv :: a -> Univ a
toUniv = Univ
toExis :: a -> Exis
toExis = Exis
useUniv :: (a -> b) -> Univ a -> b
useUniv f (Univ x) = f x
useExis :: (forall a. a -> b) -> Exis -> b
useExis f (Exis x) = f x
は、toUnivとtoExisがほぼ同じであることに注意してください。両方のデータコンストラクタは多相であるため、どちらも自由型パラメータaを持っています。返品タイプtoUnivにaが表示されていますが、返品タイプtoExisには表示されません。データコンストラクタを使用することによって得られる種類のエラーについては、存在型と汎用型の間に大きな違いはありません。
次に、ランク2のタイプforall a. a -> bをuseExisに書き留めます。これは型推論の大きな違いです。パターンマッチ(Exis x)から得られた存在型は、関数の本体に渡される余分な隠し型変数のように動作し、他の型と統一してはいけません。これをより明確にするために、統一すべきでない型を統一しようとしている最後の2つの関数の間違った宣言があります。いずれの場合も、xのタイプは、無関係なタイプの変数で統一されています。 useUnivでは、型変数は関数型の一部です。 useExisでは、それはデータ構造からの実体型です。
useUniv' :: forall a b c. (c -> b) -> Univ a -> b
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c'
-- Variable 'a' is there in the function type
useExis' :: forall b c. (c -> b) -> Exis -> b
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'.
-- Variable 'a' comes from the pattern "Exis x",
-- via the existential in "data Exis = forall a. Exis a".