lambda-calculus - haskell - Hindley-Milnerのどこが理解できないのか?

haskell / functional-programming / hindley-milner / denotational-semantics

不滅の言葉をフィーチャーしたTシャツが販売されていたことを誓います。

Arsen Khachaturyan



Answer #1

シンボルは、基本的に、あなたが何かを証明できることを意味します。したがって、 Γ ⊢ ... は、「コンテキスト Γ... を証明できます。これらのステートメントは、型判定とも呼ばれます。

では、シンボルを理解したところで、これらのルールをどのように処理しますか?これらのルールを使用して、さまざまな値のタイプを把握できます。これを行うには、式(たとえば、 f x y )を見て、ステートメントに一致する結論(下部)を持つルールを見つけます。あなたがあなたの「目標」を見つけようとしているものを呼びましょう。この場合、 e₀ e₁ で終わるルールを確認します。これを見つけたら、このルールの境界より上にあるすべてを証明するルールを見つける必要があります。これらは通常、部分式のタイプに対応しているため、基本的に式の一部を繰り返し処理します。これは、式のタイプの証明を提供する証明ツリーが完成するまで実行します。