国立情報学研究所 ソフトウェア研究系 助教授／ E-mail: ichiro@nii.ac.jp 計算モデル特論 MLの型推論 国立情報学研究所 ソフトウェア研究系 助教授／ 科学技術振興事業団 さきがけ研究21 研究員 佐藤一郎 E-mail: ichiro@nii.ac.jp

型付き言語の欠点 プログラムにおいて重要な型だけでなく、型を持つすべての式に型を記述する必要がある Lispの関数のように、一つの関数を様々なデータに対して用いたい場合がある

例：型付き言語の欠点 階乗を計算するプログラム f(x) := if x==0 then 1 then else x * f(x-1) ここで x を int 型とするとき、プログラムを見ると下記がわかる x は int型 f は int→int型 x==0 は bool型 * は int×int→int型 - は int×int→int型 if-then-else は bool×int×int→int型

例：型付き言語の欠点 Lispの関数mapcar(f, L)は、リストLの各要素に関数fを適用する mapcar(odd, [3,4]) は (int→bool)→(list(int)→list(bool)) Principe Type: (a→b)→(list(a)→list(b)) 関数twice(f, x)は関数fにxを2回適用する twice(inc 3) は (int→int)→(int→int) Principe Type: (a→a)→(a→a)

Principle Type 主型（主たる型） ある式に対する最も一般的な型付けをその式の主型と呼ぶ 例： lx.ly.x の型はたくさんの型をもつがその形はどれも a → b → a である。よってlx.ly.x の主型はa → b → a

言語ML e ::= x | n | true | false | lx.e | e1 e2 | let x = e1 in e2 | fix x.e | if e1 then e2 else e3 型 ::= a | int | bool | t1→t2 aは型変数

プログラミング言語意味論 公理的意味論（Axiom Semantics） プログラムの動作毎に作用を定式化 表示意味論（Denotational Semantics） 代数的構造にプログラムの表現（表示）を写像 操作的意味論（Operational Semantics） プログラムの動作を定式化

言語MLの操作的意味論 推論式による意味定義

型推論規則 型推論規則

let定義 (lx.e1)e2 は let x=e2 in e1に相当 型変数への型の代入（型の具体化）においてλ抽象とlet定義は相違 λ抽象の場合はそのλ式の本体に現れるλ変数の型はすべて同一の具体化を行う let定義の場合は関数適用ごとに別々に型付けが行える 　 とは t1 に出現する自由な型変数のうち、前提Γの中に出現するものを省いたa1,...,anをすべて全称限量化すること　

総称型 Generic type variable 型変数への型の代入（型の具体化）においてλ抽象とlet定義は相違 λ抽象の場合はそのλ式の本体に現れるλ変数の型はすべて同一の具体化を行う let定義の場合は関数適用ごとに別々に型付けが行える 基本データ型 整数、浮動小数点、文字、真偽値 構造データ型 配列、直積型、直和型、レコード型、ストラクチャ型 ユーザ定義型

型付プログラミング言語 プログラミング言語と型 型なしプログラミング言語 ○プロトタイピング、×インタープリタ実行 弱い型付プログラミング言語 ○手っ取り早く設計・記述、×信頼性が低い 強い型付プログラミング言語 ○安全なプログラム、×慎重な設計と冗長な記述 型検査 静的検査 動的検査

型推論 強い型付プログラミング言語を利用しながら簡潔な記述を実現するには 型は文面から推定可能 例： f(x) = if x == 0 then 1 else x * f(x-1) 推定により冗長な記述を現象 形式的な体型により型を厳密に決定

型推論の例 式要素の型と式全体の型 例： if e0 then e1 else e2 型推論の目的 与えられた式がある型を持つことを証明する 「もし e0 が真偽値型（bool型）で、e1とe2が T という型を持つことが示されれば、 if e0 then e1 else e2は T という型を持つ（ことがわかる）」 型推論の目的 与えられた式がある型を持つことを証明する 与えられた式がもつ型を求める 推論規則 e0: bool型 かつ e1:T型 かつ e2:T型 仮定 (if e0 then e1 else e2):T型 結論

型付ラムダ計算 型理論体系 項（term） 型（type） 判定（judgment） 推論規則（inference）

型付ラムダ式（基本） τ ::= b | (τ→τ) M ::= cτ | x | (λx:τ.M) | (M1 M2) BNF文法による型

型付ラムダ式 基本型: b 直積型： (τ×・・・×τ) 関数型： (τ→τ) BNF文法による型 括弧の省略 型における矢印は右結合 直積型： (τ×・・・×τ) 関数型： (τ→τ) 括弧の省略 型における矢印は右結合 例: (t1→(t2 →(t3 →t4) = t1→t2 →t3 →t4

型付ラムダ式の直感的意味 (M1 M2) (λx:τ.M) 基本式： 関数M1に引数M2を与えたときの値

型付きラムダ式の例 f(x)=x+1なる関数fは lx:int.x+1 fに実引数3を与えた式f(3)は (lx:int.x+1)(3int)

自由変数 FV(c) = 0 FV(M1 M2) = FV(M1) È FV(M2) FV(lx:t.M) = FV(M) - {x} FV(x) = {x} FV(M1 M2) = FV(M1) È FV(M2) FV(lx:t.M) = FV(M) - {x} FV((M1 ,..,M2)) = FV(M1) È .. È FV(M2) FV(M.i) = FV(M) 自由変数でない変数を束縛変数と呼ぶ

型付ラムダの計算 [N/x]c = c [N/x](M1,...,Mn) = ([N/x]M1,...,[N/x]Mn) 簡約規則 [N/x]c = c [N/x](M1,...,Mn) = ([N/x]M1,...,[N/x]Mn) [N/x](M.i) = ([N/x]M).I (lx:t.M)=(ly:t.[y/x]M) ((lx:t.M) N:t) → [N/x]M

記法 e:t A ├ e:t A1├ M1:t1 ・・・・・ An├ Mn:tn A├ M:t 前提（assumption）： 判定（judgement）: A ├ e:t （０個以上の）前提A（型環境）から、ある式eが型tを持つことが示される 推論（inference）： 式Miがそれぞれの前提Aiにおいて型tを持つならば、結論が示される A1├ M1:t1 ・・・・・　 An├ Mn:tn A├ M:t

型推論規則の記法 G+{x:t} G(x)=t 前提への操作と表記

型推論規則（詳細） 型推論規則 関数lx:t1.Mが関数型t1→t2を持つ のは、仮引数の型t1と仮定したとき、 (const) (var) 関数lx:t1.Mが関数型t1→t2を持つ のは、仮引数の型t1と仮定したとき、 関数Mが型t2をもつときである。 (abs)

型推論規則（詳細） 型推論規則 関数は、関数がその定められた値 にのみ適用可能であり、その結果 は関数の値の型を持つこと (app) 関数の組(M1,...,M2)はM1,...,M2の 直積となる (prod) 関数の組(M1,...,M2)からI番目の 要素を取り出したときはM1の型 となる (proj)

型推論の例 型推論では推論規則により変形していく 型付ラムダ式 K=lx.(ly.x)

型推論の性質 健全性 型推論できるならば、その結果が正しい（型安全）ことを意味する 完全性 正しいことはすべての型において推論することができる 有用性 決定可能かつ効率がよいこと

多相型 プログラム中に現れる同一の式やデータが複数の型をもつこと L.CardelliとP.Wegnerによる分類 アドホックな多相型 文脈によって型を決定。例、等号、オーバーローディング演算子 系統的な多相型 共通の性質をもった型に作用。例：パラメトリック多相型 パラメトリック多相型の例： twice関数　(twice f(3)) = f(f(3)) fがint型ときのtwice関数の型: (int→int)→int→int fがfloat型ときのtwice関数の型: (float→float)→float→float