type-inference - アルゴリズム W と単形型強制

Question

おもちゃの言語用に独自の型推論アルゴリズムを書こうとしていますが、壁にぶつかっています。アルゴリズム W は、過度に一般的な型にしか使用できないと思います。

式は次のとおりです。

Expr ::= EAbs String Expr
       | EApp Expr Expr
       | EVar String
       | ELit
       | EConc Expr Expr

型付け規則は簡単です。抽象化と適用のために型変数を使用します。考えられるすべてのタイプを次に示します。

Type ::= TVar String
       | TFun Type Type
       | TMono

ご想像のとおりELit : TMono、 、より具体的にはEConc :: TMono → TMono → TMono.

私の問題は、実際の型推論を行うことにあります。式構造を下に再帰する場合、 an を見るときの一般的な手法EAbsは、新しくバインドされた変数を表す新しい型変数を生成し、コンテキスト内の入力の出現を(String : TVar fresh)判断に置き換えてから、式を下に続けることです。

今、私EConcがヒットしたとき、私は同じアプローチを取ることを考えていました -サブ式の自由式変数TMonをコンテキスト内で置き換え、次にサブ式を型推論し、2 つの結果の最も一般的な単一化子を戻る主な代替。ただし、 のような式でこれを試すとEAbs "x" $ EConc ELit (EVar "x")、間違った が得られTFun (TVar "fresh") TMonます。