導入
l 強い型付けによるコンパイル時のエラー検出とプログラムの検証の利点は良く知られている。
l 強い型付けは、関数の適用が中心的な構文である関数型言語では特に自然で、そこでの型の整合性の検査はプログラムの検証の中心。
しかし
l
全ての式に意識して型を割り当てるのは大変煩雑になり得る。
→式が複合してくると式や部分式に人力で型をつけることは実質的に不可能
→型式自身も長々しくなる。
そこで
l
与えられた型のない式からシステムが型を推定する型推論というものを考える。
→ユーザーは型のないプログラミング言語のようにプログラミングできる。（柔軟性で簡潔）
応用例
l プログラミング言語MLのためのプログラミング環境において、オンラインで構文解析しながらエラーを検出してデバッグするためのツールとして役立っている。
型図式
l 関数型言語では自然に型図式(type scheme) というものが考えられる。
例：
定義 f(x)=3 ⇒ 図式 t→int （tは型変数）
定義 x(true)=z 図式 bool→s
l
ここで特に興味深い型図式は自由な型変数である型パラメータ（type
parameter）付のもの。
→総称的な手続きを書いて必要に応じて特定の型で具体化して利用できる。
例： MLのlet構文を通じて利用できる。（他の例については４節で述べる。）
principalな型推論
l プログラムから型を推論する際には、各部分式について最も一般的な（most general）型（以下principalな型という）を推定する。
l そして利用する際にそれを具体化する。
関連論文
principalな型 ← 組み合わせ論理（Curry&Feys 1958）
principalな型を求める単一化アルゴリズム ← （Robinson 1965）
principalな型が任意の組み合わせ論理の式について存在すること ← （Hindley 1969）
ML言語に対する型推論アルゴリズムW ← （Milner 1978）
形式的な計算に対するアルゴリズムWの完全な証明 ← （Dmas&Milner 1982）
1. パラメタ付き型推論
l 型推論は純粋に組み合わせ問題である。
l
仮定： 定数以外の項は型が（少なくともある時点では）決まっておらず「外部から」割り当てられる。
（その式が最初から正しく型付けされたオブジェクトとして意図されていても。）
変数の束縛
通常の項代数の様々な関数群の構文（例：λ抽象や不動点演算子μ、Martin-Lofのプログラミング言語における構文E、D、R）を、ここでは複数個の変数の束縛を引き起こす構文として一般的に取り扱う。
|
rψ=(ｐψ,ｑψ) |
rψは関数ψに対応付けられているarity（arity）、ここでｐψは関数ψで束縛されている変数の数、ｑψは関数ψの引数の数 |
項と原子型
|
＜C,Ψ＞ |
項の系（term system）を表す対。CとΨは下記参照 |
|
C=｛Ca｝a∈A =∪a∈ACa |
ここでAは原子型（atomic type）の集合、Caは型aの定数（constant）の集合 |
|
Ψ |
関数を表す文字（functional letter）の有限集合 |
式
l cが定数集合C上の任意の定数
l xが可算個の要素をもつ変数集合X上の任意の変数
l eiが式集合E上の任意の式
であるとき、
e::= c | x | ψ[x1,…,xpψ](e1,…,eqψ)となる
eはE上の式（expression）。
型構成子
Kを型構成子（type constructor）の集合とする。
仮定：型構成子は変数を束縛しない。
型式
型式（type-expression）の集合Tは
l 型変数の集合
l 型定数の集合A
l 型構成子の集合K
から再帰的に構成される。
型宣言
e∈E、τ∈Ｔであるとき式e:τは型宣言（type statement）である（eの型はτと読む）。
基底
l
かつ
であるとき
は{ei:τi}iを表す。
l
基底（basis）Bとは集合
、ここで
であって
には反復がない（）。
l B,e:τはB∪{e:τ}を意味する。
|
この定義は、「式の型はそこに含まれる自由変数の型に依存し、基底によって自由変数の型が定まる。」ことを表している。 |
型付け
l 型付け（typing）とは基底と型宣言の対B |- {e:τ}
l 基底Bによって式e中の自由変数に型が割り当てられている場合に関心があり、その場合に＜B;τ＞が式eを型付ける（＜B;τ＞typing for e）と呼ぶ。
l
一方、式e内で束縛されている変数に対する基底B内の型宣言は役に立たず、そのような変数が
に含まれないならば、＜B;τ＞の代わりに
と縮約でき、Tが式eを型付ける（T typing for e）と呼ぶ。（型の順序だけでどの変数がどの型かが決まるから。）
l 以上のような場合について、Bやσを前項（antecedent）と呼び、τを後項（succedent）と呼ぶ。
置換
l 置換（substitution）演算Sは型変数群を型式群へと出現場所に関わらず一斉に置換する。（型変数を型へと写像する。）
l
ならば
l
SRはSとRの合成で、
ならば
型推論計算
l
型推論計算（type inference
calculus）は、
各関数ψ∈Ψについて、
推論規則（inference rule）
を割り当てる。
ここで
l
これを式の形で書くと
となる。
ここで
と置換Sが具体的に定まったものは Rψのインスタンス（instance）。
型推論計算の例（λ抽象）
関数： λ
推論規則： <t; s; t→s>
式：
読み方：
「基底Bに加えて変数xの型がτという条件の下で式eの型がσ」
ならば
「基底Bの下でλx.eの型はτ→σ」
と読む。
導出
l
導出（derivation）とは型宣言のなす木Dで、
各葉はB |- c:a （ここでc∈Ca）かB |- x:σ（ここで(x:σ)∈B）であり、
各分岐ノードは推論規則のインスタンスであるようなもの。
l ある導出Dの根（root）がB |- e:τであるとき、DはB |- e:τを導く（derive）という。
principalな型付け
eに対する複数の型付けがちょうどSTの実例になるような置換Sがあれば、型付けTは式eのprincipalな型付け（principal typing for e）であるという。
注：Sが空ならST=T
|
principalな型付けは、その型付けが、さらに置換によって限定できる「広い」型を結びつけるようなものであることを示しています。 |
マルチ型拡張
l 一つの変数に複数の型を割り当てられるように拡張（基本的には非マルチ版と並行な議論）。
l 変数は１つの型にしか統制できない場合、実際の型として意図するものは変数xに割り付けた複数の型式（type scheme）の内のどれか１つ
l
Aを集合とするとき
は集合Aの有限部分集合の集まり。
l
マルチ型宣言（multi-type
statement）とは
型宣言の集合x:Σ={x:σ | σ∈Σ}（ここで
）。
l
。（置換Sは型変数の集合を型の集合へと写像する。）
l
であるとき、
である。
l
マルチ基底（multi-basis）Bとは、あるkについて集合
（ここで、
で、
に反復がない。）
l
各
が一個の要素からなる集合であれば、マルチ基底Bは基底に同型
l
マルチ型付け（multi-typing）はマルチ基底とマルチ型宣言の対B |- e:τで、
と表せる。
l
ならば
は
へ縮約できる。
l eに対する複数のマルチ型付けがちょうどSTの実例を縮約したものになる置換Sがあれば、型付けTは式eのprincipalなマルチ型付け（principal multi typing for e）であるという。
l
がマルチ基底であるとするとき、
とする。
l
マルチ型推論計算（multi-type
inference calculus）は、
各関数ψ∈Ψについて、
推論規則
を割り当てる。
ここで
l
これを式の形で書くと
となる。
ここで
と置換Sが具体的に定まったものは Rψのインスタンス（instance）。
l
導出（derivation）とは型宣言のなす木Dで、
各葉はB |- c:a （ここでc∈Ca）かB |- x:σ（ここでσ∈B|x≡Σ）であり、
各分岐ノードは推論規則のインスタンスであるようなもの。
l Σψが一個の要素からなる集合であれば、マルチ型推論計算は型推論計算と本質的に同じ。
2. パラメタ付型システムに対するMilnerの型推論アルゴリズムW
前節で定義したような任意の型推論計算のためのアルゴリズムW（Milner1978）を提示し､健全性と文法的な完全性について検討（一般化によって定義と証明は簡潔で明快になった。MLのlet構文のような束縛機構については後述。）。
2.1 型推論の戦略
例： λ計算でe=fgのfにかかる制約は：
外部制約（outer constraint）： fが現れる文脈eからくるもの
内部制約（inner
constraint）： fの構造からくるもの
両者はfとgに現れる同一の変数によって関連付けられる。
Robinson’s Unification Lemma（Robinson 1965）を利用。
l
型推論は構造に関する帰納により自然に導かれる。
の型付けは式
と規則Rψから定まり、式
に関する文脈はe自身とeに現れる自由変数
の取り得る型を制約する。
型付けアルゴリズムは与えられた式eについて、
の型列
とe:τの型τを推定しなければならない。
l
以上からアルゴリズム内の再帰呼び出しでパラメータとして
とτの両方を渡す、どちらか一方を渡す、どちらも渡さないのいずれかに応じて4つの戦略がある。
l
τは型のマッチングの最終段階で利用され､これは手続き呼び出しで実行されるのと同等なので、原子的な式向けにアルゴリズムを簡略化できる。
(1) 
がパラメータとして渡される： 
のようにSとτを探す。
→アルゴリズムW
(2) パラメータが渡されない： 
のように
とτを探す。
→再帰呼び出し１回毎に
に対する
の割り当てを再計算するので､簡単な基底が利用されている場合、相対的に効率が悪い。が、マルチ基底を利用しxiにマッチする必要があるときだけを新規に束縛するようにすれば・・・
→アルゴリズムV
l このWに対する変更によりVは概念的には簡単になっている。＋より一般的なマルチ型システムに適し､後述する連接型構成子の関連でも利点がある。
l
Vは逐次的な実装ではWと同程度の効率だが、並列実装ではより効率的。
加えて、部分式の型付けは互いに独立（subexpression disjoint thoremによる）なので部分式が変更されたときだけ型付けを変更すればより効率的。
2.2 パラメータ付型推論計算Wの定義
型推論計算を修正
入力と出力を確定する
入力： 式e、基底B
出力（中断せずに完了した場合）： 置換S、型τ
特徴
1. 健全性（soundness）： W(B,e)が成功して(S,τ)という結果を返せば､SB |- e:τが成り立つ。
2.
文法的完全性（Syntactic
compleetness）： SB |- e:τならば、W(B,e)は式eのprincipalな型付けを与える。
例：W(B,e)が結果(S0,τ0)を返せば、S=RS0、τ=Rτ0となる置換Rが存在する。
3. 実行時間はO(n2)、ここでn=|B|+|e|
単一化
RobinsonのUnification Lemma(Robinson 1965)より以下のような線形時間の手続きmatchが存在する：
かつ
ならば
が成功し、
かつK=RK0、M=RM0となるような置換Rが存在する。
|
言い換えると、置換後 Rの存在はmatchがprincipalなUnificationを行うことを表している。 |
例：(K,M)=match(τ,σ; s→t, s)かつUがτ.σ→a（aは新規）となるprincipal なUnifierとすれば、K（modulo変数変換）はUをτとσに現れる変数へだけ作用するように制限するものであり、Ua=Kτ.σ=M(s→t).s =Mtとなる。
定義
ifはDijkstraの定義による。特に適用すべき（＊）を付した節がなければ関数は中断してメッセージを返す。
適用例： e=λ[x](f)≡λx.f
C:=(B,x:s); ←外的な制約
（T,ξ）:=W(C,f); ←再帰呼び出しで得られる内的な制約
（ここでθ:=<ξ>でS:=T）
(K,M):=match(Ts,ξ;s,t);
←単一化によって外と内の制約を満たす置換を得る。
S:=KT; ←合成によって得られる最終的な置換
τ:=M(s→t);
←ψの型に単一化で得られた制約を加味した結果の型
2.3 Wの健全性
定理2.1
(S,τ)=W(β, e)が成功するならば、SB |- e:τが成り立つ。
証明
（省略）
2.4 Wの文法的な完全性
定理2.2
SB |- e:τ （ここでBはe内の自由変数
の型）ならば、W(B,e)は成功して（S0,τ0）という結果を返し、S=PS0,τ=Pτ0となるような置換Pが存在する。
証明
（省略）
補題
ならば、以下のような置換P1,…,Pjが存在する。
(1) Sρj=Pjξj
(2) S=PjSj
(3) 全ての
について Pi=PjRij
証明
（省略）
3. 文脈パラメータのない型推論アルゴリズムV
3.1 アルゴリズムVの定義
特徴
1. 健全性（soundness）： V(e)が成功して(B,τ)という結果を返せば､B |- e:τが成り立つ。
2. 文法的完全性（Syntactic compleetness）： マルチ基底BについてB |- e:τならば、V(e)は式eのprincipalな型付けを与える。
3. 実行時間はO(n2)、ここでn=|e|
マルチ単一化
定義
3.2 Vの健全性
定理3.1
(B,τ)=V( e)が成功するならば、B |- e:τが成り立つ。
証明
（省略）
3.3 Vの文法的完全性
定理3.2
B |- e:τ （ここでBはe内の自由変数
の型）ならば、V(e)は成功して（B0,τ0）という結果を返し、B=SB0,τ=Sτ0となるような置換Sが存在する。
証明
（省略）
4. 多態型の制御
· 以上で議論してきた類の型統制によって、引数がパラメータ付き型を持つ式（手続き）を定義できる。
· 残るはこのような総称的な式の利用を制御すること。
·
例：I=λx.x （型：t→t）を<I5,I true>やIIとして利用。
これは(λz.e)Iをe=<z5,z true>やe=zzとして利用すると発生。
この場合Iの総称性はzの型付けを通じて明示的に伝播する。
· 以下、異なる型の式に適用するような式の型付けを文法的に制御する仕組み（型抽象、型限量、型連接、MLのlet構文）について述べる。
4.1 型抽象
例：式eと総称型τ[t]（tは自由な型変数）
このやり方では、式eの意味が型τ[σ/t]のインスタンスの型に依存し、それが関数の依存関係として現れる。
型変数tを意識してこの抽象を行うため（関数のλ抽象に倣って）Λt.eを考える。
ΛとΔ
Λt.eは型σから型τ[σ/t]のオブジェクトe[σ/t]への関数を表し、任意の型ρへ(Λt.e)ρのように適用できる。
Λt.eの型はΔt.τと表す。そのためΔは変数を束縛する型構成子。式eが型Δt.τを持つならば、eρの型はτ[ρ/t]である。
iが型Δt.t→tを表すのならば、i型の関数xiについてxit=t→tで、xitxi=i
型抽象による制御は簡単な型パラメータから発し、オブジェクトに対する条件とオブジェクトに対する引数を共に型とすること。文法的にはこの2重性は型式利用の2層として表される。
推論規則
抽象化：
（ただし、tはBにおいて自由変数ではない）
適用：
（ただし、τにおいてσはtについて自由）
証明理論及びλ計算との関係
（省略）
4.2 型限量
型限量は：
l 全ての型τについて型τ→τを持つ式Iがあること
l この限量という属性を表す為にオブジェクトのレベルで型に関する機能を導入せずに済むこと
に基づいています。
総称的な式を複数利用できるようにするため、この暗黙の限量を明示せねばなりません。
従ってIには型Πt.t→t（「全てのtについてt→t」と読む。）が割り当てられます。
推論規則
総称化： 
（ただし、tはBにおいて自由変数ではない）
具体化： 
（ただし、τにおいてσはtについて自由）
意味
型推論の組み合わせ論の観点からは型限量は単に型抽象の記法的な変種。
定理4.1
式eを型抽象の式とし､式e’をe内で上書き、引数や抽象の対象となっている型への全ての参照を削除した結果の型付けされていない式とする。するとeが型抽象で型付けされるならば、そのときに限りe’が型限量で型付けされる。
証明
（省略・・・型抽象と型限量の推論規則から直接証明できる。）
4.3 型連接
型限量と同質の概念だが組み合わせ論的には異なる点がある。
新しい型構成子である型連接（type conjunctionあるいはtype intersection）とは：
l σとτが型ならばσ&τも型
l 式eがσ&τ型であることと、式eがτ型かつσ型であることは同値
連接されているうちのどの型が選ばれるかは文脈による。
例1：e=<z 5, z true>の場合z:(int→p)&(bool→q)だが、(λz.e)Iとなればz:(int→int)&(bool→bool)となる。
例2：zzの場合z:s&(s→t)だが、(λz.zz)Iとなればz:(q→q)&((q→q)→(q→q))となる。
型限量との関係
Iは任意の型τについてτ→τであるが、ある時点では有限個の型の連接(τ1→τ1)&,…,&(τk→τk)とも考えられる。
推論規則
連接： 
選択： 
特徴： 定理4.2
型付け可能な式は強く正規化可能なλ式（言い換えると簡約化の列が有限）
証明
（省略）
方法論的な問題点
多態を付加する際に一様性がない。
例：
式e1,…,ekがそれぞれ型τ1,…,τkを持つとする。
式<xe1,…,xek>中の変数xは(τ1→σ1)&,…,&(τk→σk)と型付けされねばならない。しかしeiの組に変更がある度に連接を掛け合わせし直さねばならない。
4.4 MLのlet構文
総称型を明示的にλz.eの変数z（e内の総称性のために利用）に割り付ける問題について考える。
アイディア
このような抽象化の式は(λz.e)dがe[d/z]へ簡約できる場合のように総称的な式で適用がある場合にのみ現れるべき。
⇒(λz.e)dをlet z=d in eと書く新しい構文を導入。
矛盾の例
正しい部分式（例：zz）にもかかわらず正しい式(例： let z=λx.x in zz)が正しくなくなる（型付けできない）ことがある。
基本的な限界
l このやり方ではパラメータ付の型による多態だけが可能：多態オブジェクトとして抽象化されている式は別の式の引数として現れてはいけない。
l
手続き呼び出しにこの制約を当てはめると：総称的な手続きを呼び出している手続きは呼び出せない。
→素朴に多態を利用するだけで、あまりにも簡単にこれを侵す例が作れる。
l これを克服するためにMLの設計者たちが考えた型推論規則については→7節
5. 限量と抽象の制御のための型推論
6. 連接の制御のための型推論
6.1 型推論の限界
6.2 型の階数と階数制限付の型推論
7. MLのlet構文に対する型推論