Hindley-Milner型推論アルゴリズムの一般化にある「ボトムアップ」型推論アルゴリズムを実装しようとしています。
6ページでは、暗黙の制約がどのようになっているのかを説明しています
t1t2単形型変数のセットに関して型を一般化することによって得られる型スキームのインスタンスである必要がありますM
ただし、9ページで、暗黙の制約に置換を適用する方法の説明中に、この単相型変数のセットに置換を適用するように指示されました。問題は、私が置換を持っている場合、[t1 := t2 -> t3]それMはもはや型変数のセットではないということです。
私はここで何を誤解していますか？
私は論文の著者と連絡を取り、彼らが私に答えを教えてくれたとき、私は少し自分自身を蹴りました：
置換関数には次の形式があるS : Substitution -> a -> aため、これを型変数のセットに適用すると、結果は型変数のセットになります。
したがって、適用するとき[t1 := t2 -> t3]は、 で置き換えるのではなく、akaでt2 -> t3置き換えます (型内の自由な型変数を取得する関数はどこにありますか)。ftv(t2 -> t3)[t2, t3]ftv
モノモーフィック型変数のセットがモノタイプのセットとしてエンコードされている場合 (裸の変数名とは対照的に)、9 ページの freevars(M) の freevars は (さらに別の) オーバーロードを必要とせず、置換の適用も必要ありません。
この点で、SOLVE の型付けは少し壊れているように見えます: activevars の定義では freevars が M に適用されますが、SOLVE では freevars は M に適用されず ("freevars(t2) - M")、M はおそらく含むことができません。型スキーム、つまりバインドされた変数があります。では、M は自由変数名の集合ですか (他の freevars(t) を使用した集合操作の前に freevars を適用する必要はありません)、それともモノタイプのセットですか (freevars を適用する必要があります) ?