[解決済み】Haskell/GHCの`forall`キーワードは何をするのですか？

質問

の仕組みが分かってきました。 forall というキーワードは、いわゆる「実存型」で使われます。

data ShowBox = forall s. Show s => SB s

しかし、これはあくまでサブセットに過ぎません。 forall このような使い方は、私には理解できません。

runST :: forall a. (forall s. ST s a) -> a

なぜこれらが違うのかを説明することも。

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

または、全体の RankNTypes のようなものを...

私は、アカデミックな環境で普通に使われるような言葉よりも、専門用語のないクリアな英語を好む傾向があります。 私が読もうとした説明（検索エンジンで見つけたもの）のほとんどは、このような問題を抱えています。

1. 不完全である。 このキーワードの使い方の一端を説明している（"実存型"のように）ので、全く違う方法でこのキーワードを使っているコードを読むまでは幸せな気分になれます（例えば、quot;実存型"のように）。 runST , foo と bar を参照)。
2. 離散数学、圏論、抽象代数のどの分野でも、今週流行っている最新のものを読んできたという前提がびっしり詰まっているのだ。 (もし私が「論文を読む」という言葉を読まなかったとしたら 何であれ の実装の詳細については、また早すぎるでしょう)。
3. 単純な概念でさえも、しばしば捻じ曲げられ、分断された文法と意味論に変えてしまうような書き方をしています。

それで...

実際の質問に移ります。 誰か完全に forall キーワードを、私が専門用語に浸った数学者であることを前提としない、明確で平易な英語で（あるいは、どこかに存在するなら、私が見逃しているそのような明確な説明を示してください）説明してください。

追加で編集しました。

以下、質の高いものから2つ目立った回答がありましたが、残念ながらベストは1つしか選べません。 ノーマンさんの回答 の理論的な裏付けを示すような説明で、詳細かつ有用なものでした。 forall と同時に、その実用的な意味合いも教えてくれました。 yairchuさんの回答 誰も言及しなかった分野（スコープ付き型変数）をカバーし、すべてのコンセプトをコードとGHCiセッションで説明してくれました。 もし両方をベストとすることが可能であれば、私はそうします。 しかし残念ながらそれは不可能で、両方の解答をよく見た結果、図解コードと添付された説明のおかげで、yairchuさんの解答がNormanさんの解答にわずかに勝ると判断しました。 しかし、これは少し不公平です。というのも、私はこの問題を理解するために両方の回答が必要だったからです。 forall は、タイプシグネチャで見たときに、かすかな恐怖を感じずにはいられません。

解決方法は？

まず、コード例から見てみましょう。

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

このコードは、プレーンなHaskell 98ではコンパイルできません（シンタックスエラー）。このコードでは forall キーワードを使用します。

基本的には、3つの 異なる の一般的な使用方法です。 forall キーワード（少なくとも、そう と思われる ) があり、それぞれ独自のHaskell拡張機能を持っています。 ScopedTypeVariables , RankNTypes / Rank2Types , ExistentialQuantification .

上記のコードでは、どちらを有効にしてもシンタックスエラーにはならず、型チェックのみで ScopedTypeVariables を有効にします。

スコープ付きタイプ変数。

スコープ付きタイプ変数は、以下のコードでタイプを指定するのに役立ちます。 where 節があります。これによって b で val :: b と同じものです。 b で foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b .

わかりにくい点 を省略した場合、そのような問題が発生することがあります。 forall は暗黙のうちに存在するのです。( Normanの回答より： "通常、これらの言語は多相型からforallを省略する" ). この主張は正しい。 しかし の他の用途について言及しています。 forall に対してではなく ScopedTypeVariables を使用します。

ランク・N・タイプ

まずはそこから mayb :: b -> (a -> b) -> Maybe a -> b は、次のものと同等です。 mayb :: forall a b. b -> (a -> b) -> Maybe a -> b , ただし の場合 ScopedTypeVariables が有効である。

つまり、すべての a と b .

例えば、こんなことをしたいとします。

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

この型は何でなければなりませんか？ liftTup ? それは liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b) . その理由を知るために、コーディングしてみましょう。

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

GHCはなぜタプルに同じ型が2つ含まれていなければならないと推論するのでしょうか？同じ型である必要はないと言ってやりましょう。

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

ふむふむ、ここでGHCは liftFunc オン v なぜなら v :: b と liftFunc が必要です。 x . 私たちが本当に欲しいのは、どんな可能性のあるものも受け入れる関数を得ることです。 x !

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

だから、それは liftTup に対して機能する、すべての x を取得する機能です。

実存的数量化。

例題を使ってみましょう。

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

Rank-N-Typesとどう違うのですか？

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

Rank-N-Typesで。 forall a というのは、表現がすべての可能な a s. 例えば

ghci> length ([] :: forall a. [a])
0

空のリストは、任意の型のリストとして機能します。

だから、実存的量子化で。 forall の中の data の定義に含まれる値は できる である。 任意の 適切なタイプであり なければならない ある すべて を使用します。