Arantium Maestum

プログラミング、囲碁、読書の話題

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

型理論 論文メモ

前回はSubstitution関連で少し寄り道したが、今回こそはPrincipal Type Schemes for Functional Programsの中核である

  • type inference
  • Robinson's unification algorithm
  • algorithm W

の話。

type inference

For assumptions A, expressions e and type-scheme σ we write

A ⊢ e:σ

if this instance may be derived from ... inference rules

以前でたAssertionにおけるA |= e:σと、今回の型推論のA ⊢ e:σの違いについては、前者が「式を評価した結果（つまり値）の型についての主張」なのに対して、後者は「式から静的に（実行することなく）導き出される型についての主張」なのがポイント。

しかし

Proposition1 (Soundness of inference). If A ⊢ e:σ then A |= e:σ.

とあり、型推論の結果は、プログラムの実行・評価の結果と一致することが証明できる。

型推論の規則は６つ：

  • TAUT （式変数の型）
  • INST （全称量化のインスタンス化）
  • GEN （自由型変数の全称量化）
  • COMB （関数適用）
  • ABS （関数）
  • LET （LET）

個人的に重要だと思えるポイントは二点。

まず、この型推論の規則はアルゴリズムではない、という点。型推論を自動的にしようと思ったら、現在の式を推論規則の下部にマッチさせて、規則の上部の式を推論していく、という流れになる。しかしINSTとABS規則に関しては一意に上部の式が決まらない。INSTに関しては「型のどの部分を全称量化のインスタンスとみなすか」ということがわからないし、ABSに関しては引数の型がわからない。型推論を自動で行うアルゴリズムには、ここら辺をうまく埋めるような追加の処理が必要になる。

もう一つのポイントはHindley Milner型推論の最大の特長であるLetによるポリモーフィズムの導入。ABSとLET規則の対比に注目するとわかりやすい：

ABSの規則：

A_x ∪ {x:τ′} ⊢ e:τ
------------------
A ⊢ (λx.e):τ′ →τ

LETの規則：

A ⊢ e:σ        A_x ∪ {x:σ} ⊢ e′:τ
---------------------------------
A ⊢ (let x = e in e′):τ

まずABSのA_x ∪ {x:τ′}とLETのA_x ∪ {x:σ}の違いが重要で、ABSは引数部分がtype、LETは変数がtype schemeとして型付けされている。typeとtype schemeの違いは全称量化子が出てこれるかどうかなので、LETの場合のみ導入される変数が多相な型として推論され得ることがわかる。

そしてなぜLETではそのような推論が可能でABSでは無理か、というとLETの場合は上部に追加でA ⊢ e:σがあり、変数のtype schemeはそこから来ている、ということがポイントになっている。ABSの場合は引数の型はどうにかして関数のボディの方から推論しなくてはいけないのに対して、LETではlet x = e in e'のeの式に対して型推論して、そのtype schemeを使えばいい。

Robinson's Unification

次に必要になるのは、型変数を含むかもしれない二つの型がunifyできるか（型変数への任意の代入で同一の型にできるか）を調べ、unifyできるとしたらその型変数の変換を表すSubstitutionを返すUnificationアルゴリズム：

... we require the unification algorithm of Robinson [6].

Proposition 3 (Robinson). There is an algorithm U which, given a pair of types, either returns a substitution V or fails; further

(i) If U(τ,τ′) returns V , then V unifies τ and τ′, i.e. V τ = τ′.

(ii) If S unifies τ and τ′ then U(τ, τ′) returns some V and there is another substitution R such that S = R V.

Moreover, V involves only variables in τ and τ′.

Unificationの対象になるのはtype schemeではなくtypeであることに注意。

実はPrincipal Type Schemes for Functional Programsではアルゴリズムの詳細が出てこない・・・　Robinsonの元の論文は1965年のA Machine-Oriented Logic Based on the Resolution Principleのようで、効率が非常に悪いのでその後の研究で出たMartelliとMontanariのAn Efficient Unification Algorithmなどで代用されるのが普通のようだ。

型推論を実装したい場合、Unification部分はこの論文以外から持ってくる（あるいは自前で実装する）必要がある。

Unificationの条件で気になるのはこの部分：

(i) If U(τ,τ′) returns V , then V unifies τ and τ′, i.e. V τ = τ′.

これだと(α_1 -> int)と(int -> α_2)がunifyできないように見える。というのはSubstitutionは必ず型変数から型への変換なので、V τ = τ′のような片方のみへの適用だと片方の型変数はintにできるが、もう片方の型変数は残ったまま、かつintを型変数に変換することはできない、というわけでunificationが失敗してしまう。正しくはV τ = V τ′ではないか？

ちなみに前回悩んでいたSubstitutionにSubstitutionを適用する話だが、Unificationの条件２を見ると：

(ii) If S unifies τ and τ′ then U(τ, τ′) returns some V and there is another substitution R such that S = R V.

となっていて、例えばVが[int/α_1]でSが[int/α_1, int/α_2]だった場合[int/α_1, int/α_2] = [R int/α_1]というのは如何なるRでも成り立たない。なのでSubstitutionにSubstitutionを適用するのはS = R ++ [R τ_i/α_i]が正しいはず。

Algorithm W

ついにアルゴリズムWについて。

まず、何をするアルゴリズムかというと：

Given A and e, if W succeeds it finds a substitution S and a type τ, which are most general in a sense to be made precise below, such that S A ⊢ e:τ.

アルゴリズムの内容は、式の形に対するパターンマッチだ。この記事ではパターンマッチの項目ごとにOCamlの擬似コードを書いていく。

ちなみに：

There are obvious typographic errors in parts (ii) and (iv) which are in the original publication. I have left the correction of these as an easy exercise for the reader.

とのことなので、擬似コードの方は（多分正しく？）修正してある。

まずは冒頭：

W (A,e) = (S,τ) where

let rec w assumptions expr = match expr with

式が変数の場合：

(i) If e is x and there is an assumption x:∀α1,...,αnτ′ in A then S = Id and τ=[βi/αi]τ′ where the βis are new.

| Var x -> (match find x assumptions with
  | Some (generic_vars, ty) ->
    let new_vars = make_new_vars (List.length generic_vars) in
    let ty = substitute_type (List.combine generic_vars new_vars) ty in
    ([], ty)
  | None -> failwith "Variable not found in assumptions")

式が関数適用の場合：

(ii) If e is e1 e2 then let W(A,e2)=(S1,τ2) and W(S1 A, e2)=(S2,τ2) and U(S2 τ1, τ2→ β)=V where β is new; then S=V S2 S1 and τ=Vβ.

| Call(e1, e2) ->
  (let s1, ty1 = w assumptions e1 in
   let s2, ty2 = w (substitute_assumptions s1 assumptions) e2 in
   let beta = make_new_var () in
   let v = unify (substitute_type s2 ty1) (TyAbs(ty2, beta)) in
   ((merge_substitution v (merge_substitution s2 s1)), (substitute_type v beta)))

式が関数の場合：

(iii) If e is λx.e1 then let β be a new type variable and W(Ax∪{x:β},e1)=(S1,τ1); then S=S1 and τ=S1β→τ1.

| Lambda(var1, e1) ->
  let beta = make_new_var () in
  let s1, ty1 = w ((var1, beta) :: (remove var1 assumptions)) e1 in
  (s1, TyAbs(substitute_type s1 beta, ty1))

let式の場合：

(iv) If e is let x = e1 in e2 then let W(A,e1)=(S1,τ2) and W(S1Ax∪{x:S1A(τ1)},e2)= (S2,τ2); then S = S2 S1 and τ = τ2.

（注：{x:S1A(τ1)}は正しく表示されないが、論文の中ではS1Aの上に横線があり、closure of τ1 in S1 Aである）

| Let(var1, e1, e2) ->
  let s1, ty1 = w assumptions e1 in
  let s2, ty2 = w ((var1, (closure (substitute_assumptions s1 assumptions) ty1)) :: (substitute_assumptions s1 (remove var1 assumptions))) e2 in
  (merge_substitution s2 s1, ty2)

パターンマッチに合致しないケース：

NOTE: When any of the conditions above is not met W fails.

| _ -> failwith "Failed to match patterns for algorithm W"

Unificationの内容はまだはっきりしないが、それ以外の部分は論文に従うだけで比較的簡単に実装できそう。（まだsubtitute_Xやclosureなどのヘルパ関数は実装できていないが、これらはそう難しくないはず）

Principal type scheme

ちなみにタイトルにもある通り、この論文の主眼は「プログラムのprincipal type schemeを推論したい」というもの。

そもそもprincipal type schemeとは何か？

Given A and e, we will call σp a principal type-scheme of e under assumptions A iff

(i) A ⊢ e:σp

(ii) Any other σ for which A ⊢ e:σ is a generic instance of σp.

要約するとA ⊢ e:σpを満たすもっともジェネリックなtype scheme、ということになる。

アルゴリズムWはprincipal type schemeを推論する、というのが重要な結果：

Our main result, restricted to the simple case where A contains no free type variables, may be stated as follows:

If A ⊢ e :σ for some σ, then W computes a principal type scheme for e under A.

ちなみに証明はこの論文には載っておらず、

The detailed proofs of results in this paper, and related results, will appear in the first author’s forthcoming Ph.D. Thesis.

とのこと。まあ実装する分にはそこまで重要ではないとも言える。

まとめ

というわけで主要な概念とアルゴリズムWの実装の大筋がわかった。Unificationについては別の記事で実装も含めて見ていきたいと考えているが、それ以外では自作言語に型推論をつけるための最低限の道具立ては整ったはずなので楽しみ。