Seminar / Milner's paper

型多相の理論

宣言なしに型を決め、しかも実行時に「型が壊れない」ことを証明する

Robin Milner, A Theory of Type Polymorphism in Programming,
Journal of Computer and System Sciences 17(3), 348–375, 1978.
概要：児玉靖司（東京理科大学理工学部情報科学科）／ Part I・II・III

§ 1

柔軟さと安全さは両立するか

この研究は実際的なものである — 論文の第一文。

型を強制しない言語には柔軟性がある。しかしその柔軟性のせいで、広い意味で「機能する手続き」を定義するのに注意が要る。Lisp では CDR をミスするかもしれない。ALGOL68 は ALGOL60 が持っていた柔軟性を排除する方向で答えを出した。Milner が探すのは第三の道である。

Strachey は初期の「柔軟性」の議論で、おそらく最初に多相性 (polymorphism) を唱えた。彼はパラメトリック多相を定義し、それ以外をアドホック多相とした。+ に整数の加算と実数の加算を与えるような扱いは今日オーバーローディングと呼ばれるが、この論文はオーバーローディングも型強制 (coercion) も扱わない。これらは実行時の扱いであると考えるからである。

この論文の主張

プログラムに出現する多相性は、すべてのプログラミング言語に存在するプリミティブな演算子 — 代入、関数適用、組 (pairing, tupling)、リスト処理 — の自然な産物である。CLU・ALPHARD・Euclid のようにユーザが型を定義する近年の言語に対して、ここで提案する型は大変シンプルである。

型を書かないこと

型の処理はコンパイル時に行われる。型チェッカがプログラムを受理したら、実行時に型を扱わないコードを生成してよい。そしてプログラム全体に型を指定することはしない。型はプログラムのコンテキストから推論される。Tennent は型変数や識別子には型を指定する必要があると主張したが、本論文は指定しない側に立つ。

由来

ここで議論する型の規則 (discipline) は、LCF のメタ言語 ML において導入されたものである。研究の後で、著者らは Hindley がコンビナトリロジックの項に対する「主要な型スキーマ」を導出していたことに気づいた。Hindley は Robinson の単一化アルゴリズムがこの問題を解くのに適していると気づいた最初の人であろう。本研究は Hindley の方法を局所的な定義を持つプログラミング言語に拡張し、その方法に意味論的な正当化を与えるものである。

論文の構成

  • §2 ML のプログラム断片で、例により型の規則を概観する（self-explanatory な節）。
  • §3 簡単な言語 Exp を導入し、well typing（正しい型割り当て）の概念を定義して、意味論的健全性（well-typed なプログラムは意味論的に型エラーを起こさない）を証明する。
  • §4 well-typing を求めるアルゴリズム 𝒲 を提案し、文法的健全性（𝒲 が成功すればプログラムの well-typing を生成する）を証明する。さらに 𝒲 をシミュレートする、より効率的なアルゴリズム 𝒥 を提案する。
§ 2

型規則の概要

例が語る節。map と tagpair の二つで、この型システムの骨格はほぼ尽きる。

宣言は let x = e in e′ と let f(x1,…,xn) = e in e′ の形をとり、後者は値（抽象）λ(x1,…,xn)·e を f に与える。再帰関数には let の代わりに letrec を使う。

単相型 (monotype) は、中値二項演算子 ×（カルテシアン積）と +（和）、→（関数型）、後置単項演算子 list により、基本型（int, bool など）から構築される。多相型 (polytype) は、そこに型変数 α, β, γ を許すことで導入される。

例 1 — リスト上の map

letrec map(f,m) = if null(m) then nil
                else cons(f(hd(m)), map(f, tl(m)))

この生の宣言から、どのように型が決まるのか。まず自由な識別子の generic 型は

null : α list → bool,   nil : α list,   hd : α list → α,   tl : α list → α list,   cons : (α × α list) → α list

である。各型は一つ以上の型変数を持つので多相型であり、そのような識別子のすべての出現の generic 変数に対して、置換したインスタンスである型を代入することができる。宣言の中でちょうど一回出現する識別子には σnull = τ1 list → bool のように型を割り当て、二回以上出現する map, f, m についても同様に型変数を置いて等式を並べる。Morris はそのような等式の解を議論したが、この設定は Robinson の単一化アルゴリズムの使い方にちょうど適していた。Robinson の研究より、求める解は map の most general type であると結論づけられる。実際の解は

ρmap = (γ → δ) × γ list → δ list

であり、γ, δ は独立した型変数である。これが map の generic type であって、この宣言のスコープの中でのあらゆる map の出現には、この型の置換によるインスタンスが割り当てられる。これらのインスタンスは同一である必要はない。 tok を基本型として length : tok → int, sqroot : int → real とすると

map(sqroot, map(length, tokl))

と書くことができ、上の 2 つの map は別々の型 ((tok → int) × tok list) → int list と ((int → real) × int list) → real list を持つ。一方で、異なった位置に出現する仮引数や、再帰的に定義された識別子（map 自身）は、同じ型としなければならない。

この導出を導出器で動かす →

例 2 — tagpair と、λ 束縛の落とし穴

関数 tagpair : (b,c) ↦ ((a,b),(a,c)) を考える。素直には let tagpair(a) = λ(b,c)·((a,b),(a,c)) と定義でき、型は

α → (β × γ → (α × β) × (α × γ))   … (*)

となる。別の方法で定義してみる。(f # g)(a,c) = (f(a), g(c)) により # を、pair(a)(b) = (a,b) により pair を用意して

let tagpair = λ·(let tag = pair(a) in tag # tag)

とする。ここで もし局所的な tag の generic type を使って、tag # tag の 2 つの出現に別々の型を割り当てると、tagpair の型は

α → (β × γ → (α1 × β) × (α2 × γ))   … (**)

になってしまう。何かが間違っている。第二の型は too general である。tag とその generic type は λ 束縛された変数 a に依存している。λ 束縛された変数に対して、異なった型を割り当てるべきではない。

結論（この論文の核）

let と letrec により束縛された変数の型にのみインスタンシエーションすればよい。より正確には、λ 束縛された変数や、仮引数の束縛ではない型変数にのみインスタンシエートする。上の例で明らかになったのは、let（または letrec）と λ は異なった扱いをしなければならないことである。let x = e in e′ と (λx·e′)e は意味論的には同じであるが、型を正しく割り当てる場合は前者のやり方が可能になる。

例として let I = λx·x in I(I) と (λI·I(I))(λx·x) をあげることができる。λ 束縛と let 束縛の扱いをどうするかが、このアプローチの核である。

let 版を動かす → λ 版（失敗する）→ tagpair の (*) と (**) →

well type にならない有益な式

カリーの Y コンビネータ Y = λf·(λx·f(x(x)))(λx·f(x(x))) は self-application なので ill typed となる。この体系では letrec を使うことにより Y を使わなくてもよくしている。他の例として

let F(f) = λ(a,b)·(f(a), f(b))

に対し F(reverse)(x,y) を考える。これにより異なった型を持ってよい 2 つのリバースリストが生成されるはずだが、我々のシステムではこのような定義は許されない（λ 束縛である a, b は同じ型でなければならない）。しかし次のようにして回避することができる。

let reversepair = λ(x,y)·(reverse(x), reverse(y))

この例は、我々のシステムの主な制限を概観している。

Y コンビネータの失敗を見る → reversepair →

§ 3

言語 Exp と、意味論的健全性

例で示した規則を、簡単な言語の上で正確に述べ、証明する。

3.1 言語 Exp

e ::= x | (e e′) | if e then e′ else e″ | λx·e | fix x·e | let x = e in e′

(e e′) は適用、fix x·e は λx·e の最小不動点、最後は let-in-end を意味する。定数は省略する。

Exp には通常の表示的意味を与えることができ、そこでは wrong（実行時の失敗）を含んでいる。この小さな言語では、失敗とは、条件式の条件部に論理値でない値が出現した時と、適用の演算として関数でない値が出現した場合のみである。各意味領域は cpo（complete partial order）であり、基礎領域の集合 {Bi}（B0 = T）に対して

V = B0 + B1 + ⋯ + F + W,   F = V → V,   W = {·}（エラー）

と再帰的に定義する。この解は Scott により確かめられた（cpo で解いたのは Plotkin である）。意味関数は ℰ ∈ Exp → Env → V、Env = Id → V である。

3.2 Exp の意味等式

要点だけを挙げる。ℰ⟦λx·e⟧η = (λv·ℰ⟦e⟧η{v/x}) in V、ℰ⟦fix x·e⟧η = Y(λv·ℰ⟦e⟧η{v/x}) であり、ここで Y は最小不動点演算子である。多くの言語では fix f·e の e は抽象 λy·e′ に制限されている。そのため let f = fix f·(λy·e′) は let rec f(y) = e′ と書くことができる。

ℰ のもとでは let x = e1 in e2 は (λx·e2)e1 と同じ意味であることを確かめることができる。しかし我々の目的の一つは型規則であり、そこでは両者は違う。また (e1 e2) の意味論は値渡しである（e2 が ⊥V なら (e1 e2) も ⊥）。このテストを省略すると名前呼出しとなるが、意味論的健全性はこの場合も同じである。

3.3 型に関する議論 / 3.4 型とその意味

値は多くの型を持つかもしれないし、全く型を持たないかもしれない。wrong は型を持たない。一方、関数値は型を持つ — 引数が正しい kind に適用される限り、正しい kind を生成し、wrong にはならない。したがって「Exp の式は（適切な環境において）型を持つ値として評価することができ、wrong にはならない」ことを示せばよい。ここで二つの作業がある。(i) 正しい型割り当てを持つ式は wrong にならないことを示すこと。(ii) 正しい型割り当てを見つけること（型チェック）。

型の文法は基礎型 ι0, ι1, …、型変数 α, β, γ、および ρ → σ からなる。値 v ∈ V が単相型 μ を持つことを v : μ と書き、

v : ιi  iff  v = ⊥V または v ∈ Bi   ／   v : μ → ν  iff  v = ⊥V または、v ∈ F かつ (v|F)u : ν (u : μ の時つね)

と定める。多相型に対しては ρ ≪ σ（ρ は型変数への置換により σ から得られる）を用いて v : ρ iff ∀μ ≪ ρ · v : μ と定義する。≪ は反射的・推移的である。全称量化は outermost にのみ存在するものとし、(∀α·α → α) → α のような型は考えない — Reynolds の richer notion における難しさを避けるためである。⊥V はすべての型を持つ（すべての型を持つ唯一の値である）。

3.5 型割り当て — prefixed expression と wt

prefix p は let x, fix x, λx をメンバとする有限の列である。prefixed expression (pe) は p|e という形を持ち、e の自由変数は p のメンバとして出現する。各 pe は再帰的に定まるサブ pe を持つ。たとえば λy|(let f = λx·(xy) in (fy)) は、自分以外に λy|λx·(xy), λy·λx|(xy), λy·λx|x, λy·λx|y, λy·let f|(fy), λy·let f|f, λy·let f|y をサブ pe として持つ。

generic 型変数の定義

型付けされた pe p̄|ēσ において、束縛 let xσ の中の型変数が、閉じた λyτ または fix yτ に出現しない時、その変数を let xσ に対して generic であるという。直感的には、束縛された x に対して generic な型変数は、x が使われる型の自由さの度合いを表現している。つまり x の局所的な多相性である。let xσ により閉じられた時に λ や fix の束縛がない場合は、σ にある型変数はすべて generic である。

well-typed (wt) は 6 つの場合による再帰的定義で与えられる。とくに：

  • p̄|xτ が wt iff standard であり、かつ p̄ の中で λx または fix xτ が active であるか、let xσ が active で τ が σ の generic instance であるとき。
  • p̄|(ēρe′ρ′) が wt iff 両方とも wt かつ ρ = σ → τ。
  • p̄|(λxρ·ēσ)τ が wt iff p̄·λxρ|ē が wt かつ τ = ρ → σ。
  • p̄|(let x = ēρ in e′σ)τ が wt iff p̄|ē と p̄·let xρ|e′ が共に wt、かつ σ = τ。

ここで standard とは、すべての型付けされたサブ式 p̄′|d̄′ に対して、p̄′ の各メンバ let xσ の generic な型変数が p̄′|d̄′ に出現しないときをいう。

3.6 置換

置換 S は型変数から型へのマップであり、自然に型から型へ、型のついた pe から pe へのマップも示す。

命題 4

もし S が wt な p̄|d̄ の generic variables を含まないならば、S(p̄|d̄) もまた wt である。

3.7 well-typed な式は wrong にならない

意味論環境 η と型環境 p̄ の関係を定める。η respects p̄ とは、let xρ または λxρ, fix xρ が p̄ において active であり、η⟦x⟧ : ρ であるときをいう。

定理 1 — 意味論的健全性

もし η respects p̄ かつ p̄|d̄τ が well typed の時、ℰ⟦d⟧η : τ。

系：ℰ⟦d⟧η ≠ wrong（wrong は型を持たないから）。

証明は d̄τ の構造に関する帰納法で、6 種類の場合を見る。λ の場合には命題 4 が効く（p̄·λxμ で generic でない型変数への置換 S を考えて wt を保つ）。fix の場合は v = Y(λv′·ℰ⟦e⟧η{v′/x}) に対して v0 = ⊥V, vi+1 = ℰ⟦e⟧η{vi/x} とし、型の directed completeness より各 i に対して vi : ρ を示せばよい。

§ 4

アルゴリズム 𝒲 とその正当性

「well typing を見つける」という問いに挑戦する節。

命題 5 — Robinson

式のペア σ と τ に対して、以下を満たす置換 S を生ずるアルゴリズム 𝒰 がある。

  1. もし 𝒰(σ,τ) が成功したとすると、U は σ と τ を単一化する（Uσ = Uτ）。
  2. もし R が σ と τ を単一化すると、𝒰(σ,τ) が成功し、ある置換 U を生成することができる（R = SU）。

プログラム f の well typing を見つけるためには、型付けされた prefix p̄ を仮定しなければならない。𝒲 は p̄|f̄ が wt である f̄ を生ずると期待する。𝒲(p̄, f) = (T, f̄) は置換 T を返し、必要な変換を示す。正確には 𝒲(p̄,f) が成功して (T, f̄) を返したとき、(Tp̄)|f̄ は wt である。previously に出現しなかった新しい型変数を βi で表す。𝒲 は f に関して帰納的に定義される。

4.1 𝒲 の健全性のための道具

A が型・型付けされた prefix または pe のとき、

Vars(A) = {α | α ∈ A, α は型変数},  Gen(A) = {α | α ∈ A, α は generic な型変数},  Spec(A) = Vars(A) − Gen(A)

S が置換のとき Inv(S) = {α | S は α を含む}。命題 6：Inv(RS) ⊆ Inv(R) ∪ Inv(S)、Vars(Sτ) ⊆ Vars(τ) ∪ Inv(S)。

定理 2 — 文法的健全性

p̄ を standard な prefix とし、p|f を閉じた pe とする。その時、もし 𝒲(p̄,f) = (T, f̄τ) ならば、

  1. (A) Tp̄|f̄τ は wt。
  2. (B) Inv(T) ⊆ Spec(p̄) ∪ New。
  3. (C) Vars(τ) ⊆ Spec(p̄) ∪ New。

ここで New は 𝒲 で使われる新しい型変数の集合を示す。証明は wt の再帰的な定義を使って f の構造による帰納法で行う（条件式と fix の場合は省略）。let の場合には、Gen(Rp̄) = Gen(p̄) を得て Vars(ρ) と独立であることから Rp̄·let xσ が standard prefix であることが効く。

健全性のためには 𝒲 が成功するときはいつも wt であること、完全性のためには wt が存在するときはいつも 𝒲 が少なくとも一つ見つけることができること、を示す。𝒲 は（多分）完全であるが簡単な証明は難しく、本論文では健全性に絞る。𝒲 の完全性の証明には命題 5 の第二の部分が必要になるが、健全性の証明では第一の性質のみでよい。

𝒲 をシミュレートする型チェックアルゴリズム 𝒥 は、LCF のメタ言語 ML として 2 年間成功している。その有用性が証明されている。実際、最後に紹介する 𝒥 は大変シンプルになっている。

導出器

証明の過程を、実際に変形する

アルゴリズム 𝒲 を 1 ステップずつ実行します。単一化が型変数を束縛するたびに、木全体の型が書き換わっていく様子がそのまま見えます。

式
初期の型環境を見る

論文 §2 の例に合わせた識別子。tok は基本型、# は中置で書けます。

ステップ
0式を入力すると導出が始まります。
現在の置換 S
規則をいじる
導出木  p̄ | e : τ
いま変形された部分 prefix の let 束縛で generic な型変数 適用した規則 ← / → キーで 1 ステップ

各行は「規則 ／ 式 ／ 割り当てられた型」。いま処理しているノードの下には、論文 §3.5 の prefix p̄（λ / fix / let の束縛とその型）を展開しています。型は毎ステップ、その時点の置換 S を通して描かれるので、単一化が 1 つの型変数を束縛すると、木全体の型が同時に書き換わります。組 (e, e′) と λ(x,y)·e は §2 の例（map, tagpair）を書くための拡張です。

命題 5

単一化アルゴリズム 𝒰 を単体で動かす

導出器の心臓部。二つの型を与えると、most general unifier を求める過程が出ます。

書き方：a -> b（→）、a * b（×）、a list、int / bool / real / tok は基礎型、それ以外の名前は型変数。

その後

この論文が残したもの

本論文の型システムは今日 Hindley–Milner 型システムと呼ばれ、𝒲 は Algorithm W としてそのまま教科書に載っている。let 多相、principal type、単一化による型推論という 3 点セットは、ML から SML・OCaml・Haskell・F# へ、さらに Rust や TypeScript の局所的な型推論へと受け継がれた。

同時に、論文が自ら認めた制限もそのまま残った。λ 束縛の引数は多相にできない（F(f) = λ(a,b)·(f(a),f(b)) の例）。これを越えるには Reynolds の System F 系の「richer notion」が要るが、そこでは型推論が決定不能になる — 本論文が全称量化を outermost に限り、意図的に避けた地点である。推論できる範囲で最大の多相性を採るという判断が、この設計の中心にある。

また Milner はここで完全性の証明を保留した（「多分完全であるが簡単な証明は難しい」）。完全性は後に Damas と Milner (1982) によって与えられ、型システムは Damas–Milner として定式化される。

この体系の要点を三行で

  1. 型変数を置き、等式を立て、単一化する。解は most general type になる。
  2. 一般化してよいのは let / letrec 束縛だけ。λ 束縛の変数に依存する型変数は generic にしない。
  3. それで得た型付けは、値の型を「wrong を含まない値の集合」と読むことで、意味論的に正当化される。