「構造的部分型と有界量化に関する型推論」からリンクされているsubtyping.pdfにはいくつかの誤謬・誤植や非自明な点があると感じました。
ページ10の θΓ := {x ↦ θτ | (x ↦ τ) ∈ Γ} でτが用いられていますがσが適切ではないでしょうか。
説明なくθ ∘ θ'のような合成がされています。
次のように定義されるでしょう。
(θ ∘ θ')α :=
θτ (α ↦ τ) ∈ θ' である場合
τ (α ↦ τ) ∈ θ であり、α ∉ dom θ' である場合
θΓを定義するために必要です。
θ(∀α :: κ. σ) :≡ ∀α :: θκ. θσ α ∉ FTV(θ) かつ α ∉ dom θの場合
適宜α変換を行うことによって全域的な操作とすることができます。
FTV(∀α :: κ.σ) := FTV(σ) ∪ FTV(κ) ∖ {α}
実際の実装では順序付き組を用いて表現するので、図4に書いてある通りに実装するとUnifyAux関数の引数のパターンマッチに失敗してしまうことがあります。
ページ6の置換の定義では変数捕縛が起きてしまうと思います。
(実装方法によっては、かつInfer(∅, ∅, e)しか実行しない場合は、変数捕縛に注意を払わずに実装しても問題が起きないため厄介です。)
図2のInfer関数の「項が関数適用」であるケースでβ := FreshTypeVar()とした後に種環境をβ ↦ Uで拡張しないと、種環境に存在しない型変数が発生してしまいます。
図4のUnifyAux関数において、α1 ≟ α2の形をした制約を扱う際、
K' := ([α2/α1]K)[α1 ↦ ...]
となっていますが
K' := ([α2/α1]K)[α2 ↦ ...]
が正しいと思われます。
10ページ目のClose関数に誤りがあります。
(FTV(K) ∪ FTV(τ)) ∖ FTV(Γ)
となっていますが、
EFTV(K, τ) ∖ EFTV(K, Γ)
が適切かと思われます。
EFTVは(Ohori 1995)で定義されていて、essentially free type variablesを表すものであり、次の二つの条件を満たす最小の集合です(表記はsubtyping.pdfに合わせています)。
1. FTV(σ) ⊆ EFTV(K, σ).
2. if α ∈ EFTV(K, σ) then FTV(K(α)) ⊆ EFTV(K, σ).
これはΓにも自然に(FTVと同じように)拡張されます。
現在のClose関数の定義のままだと、例えば
e ≡ (λx. let y = (λz. f (x#r) z) in x#r)
Γ ≡ Γ'[f ↦ ∀α :: U. α → α → α]
であるとき、Infer(K, Γ, e)で型を推論することができない(はず)です。
また8ページ目の図1のΛα : κ. Mに対する型つけ規則において、α ∉ FTV(Γ)はα ∉ EFTV(K[α ↦ κ], Γ)に置き換えられるべきです。(Ohori 1995)ではFTVが用いられています(Fig. 5)が、それはα ∉ dom Kであることを前提にしているからです。
図4のUnifyAux関数は{R} ≟ {R} (両方がレコード型)であるケースにも対応するほうが良いかもしれません。
閉じた項をInfer関数に渡したときにそのような制約が発生することはないと思われますが、
型環境に{R} → τ型の項がある場合(や、「明示的に型を指定する仕組み」(例えばλx:τ.Mのようなλ抽象)を追加した場合)に発生し得ます。
Atsushi Ohori. A Polymorphic Record Calculus and Its Compilation. ACM Transactions on Programming Languages, vol. 17, no. 6, 844–895, 1995.