[解決済み] Hindley-Milnerのどの部分が理解できないのでしょうか？

質問

I 誓う 以前は Tシャツ という不朽の名言を残しています。

のどこが？

してください じゃない がわかるか？

私の場合、答えは...全部！です。

特に、Haskellの論文でこのような表記をよく見かけますが、どれがどういう意味なのかさっぱりわかりません。数学のどの分野なのか、さっぱりわからない。

ギリシャ語のアルファベットはもちろん、quot;∉"（これは通常、何かが集合の要素ではないことを意味します）などの記号は分かりますが。

一方、"⊢は見たことがないですね( ウィキペディアでは、「パーティション」という意味かもしれないとしています。 ). また、ここでのヴィンキュラムの使い方もよくわからない。(通常、分数を表しますが、これは 現れる ということです)。

この記号の海が何を意味するのか理解するためには、少なくとも何から始めればいいのか、誰かが教えてくれれば助かるのですが。

どうすればいい？

• その ホリゾンタルバー は、"[above]を意味します。 を意味する [以下]"。
• がある場合 複数の表現 を[上]のように考えてください。 とした。 を保証するためには、[上]がすべて真でなければならない。
• : 意味 はタイプを持っています
• ∈ 手段 があります。 . (同様に ∉ は、"is not in"を意味します)。
• Γ は、通常 環境 この場合、識別子とその型のペアリングを行う型注釈のセットと考えることができます。したがって x : σ ∈ Γ というのは、環境 Γ という事実が含まれています。 x は、タイプ σ .
• ⊢ と読むことができます。 証明する または決定する。 Γ ⊢ x : σ というのは、環境 Γ が決定する。 x は、タイプ σ .
• , は を含む 環境に特定の付加的な仮定を加える Γ .
  したがって Γ, x : τ ⊢ e : τ' というのは、環境 Γ , という仮定が追加され、上書きされます。 x は型 τ は、以下のことを証明しています。 e は、型 τ' .

ご要望にお応えして、演算子の優先順位を高いものから順にご紹介します。

• 言語固有の infix および mixfix 演算子、たとえば λ x . e , ∀ α . σ および τ → τ' , let x = e0 in e1 および関数アプリケーションのための空白文字。
• :
• ∈ そして ∉
• , (左結合)
• ⊢
• 複数の命題を区切る空白（連想）
• 横棒