Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む（中編）

前回「type inference、Robinson's unification, algorithm Wを見ていく」と書いたが、その前にsubstitutionについてつらつらと考えてみたい。

S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i]

とある通り、substitutionは型変数から型へのマッピングだ。typeはτ ::= α | ι | τ → τなので、自由な型変数が出てくることも可能。極論すれば[α_1/α_1]のようなsubstitutionも定義上は可能だし、[α_1/α_2, α_2/α_1]のようなsubstitutionもあり得る。

後者のようなsubstitutionだと、適用する順序が結果を変える可能性があるか？とも思ったのだが

If S is a substitution of types for type variables ..., and σ is a type-scheme, then Sσ is the type-scheme obtained by replacing each free occurrence of α_i in σ by τ_i

とある。字義通りに読むならeach free occurrence of α_i in [τ_1/α_1,...,τ_(i-1)/α_(i-1)]σではないので、順番は関係なさそう。

つまり[α_1/α_2, α_2/α_1](α_1 -> α_2)は(α_2 -> α_1)になるはず。

次に

S = RV

の解釈について考えたい。（S, R, Vはすべてsubstitution）

substitutionなので最終的にはtype schemeに適用するわけだ。つまりRVσのような形になる。

ここで「まずσ'=Vσと適用して、Rσ'を返す」という処理はあり得るだろうか？

S = RVと論文に出てくるので、RVは一つのsubstitutionとして表せるはず。

一番簡単な表し方は単に二つのsubstitutionをappendすることだが、そうするともしVの型の中にRでsubstituteされる型変数が含まれている場合、「まずσ'=Vσと適用して、Rσ'を返す」という結果にはならない。

なのでV=[τ_i/α_i]とすればV'=[R τ_i/α_i]とVの型にRを適用した新しいsubstitution V'を用意した上で、SはRとV'のconcatenationという形になるはず。

もう一つの解釈としてはS=V'そのまま。Substitutionとしてはむしろこれが素直な解釈か？ただし、Rの型変数がその後適用されるσに出てきてもsubstituteされないということになるが・・・

まとめると

V = [τ_i/α_i]

だとして

S = RV

の解釈としては

S = R ++ V
S = [R τ_i/α_i]
S = R ++ [R τ_i/α_i]

の三通りが考えられ、後者二つが最もあり得そう。素直なのは二番目、一番汎用性がありそうなのは三番目。Principal Type Schemes for Functional Programsでどちらが使われる想定なのかはAlgorithm Wの詳細を見ていけばわかるはず（そうだといいなぁ）。

というわけで次こそはtype inference、Robinson's unification、そしてalgorithm Wの詳細の話。