Document

型推論１（単相型）
2007
型推論へ１
強い型付言語の記述
上の煩瑣さを軽減
型推論へ２
型推論へ３
型推論の形式的体系について
• 形式的な記号の集まりからなる論理体系
• プログラムの文面を含んだ体系(cf. Hoare logic)
• 体系の重要な要件
（１）健全性（２）完全性
（３）推論アルゴリズムの有用性 → a)決定性 b)効率
• 「値」の正当性と「型」の正当性の比較
型推論規則のアイデア（例）
E0, E1, E2を式として、
もし E0が bool式であることが示され
かつ E1の型がTであることが示され
かつ E2の型がTであることが示されたなら
その時、式if E0 then E1 else E2は型Tをもつことが示され
る
これを
形式化して
1. 与えられた式がある型をもつことを証明する(prove)
2. 与えられた式がもつ型を見つける/推論する(find/infer)
言語の型システムを与えるとは
• 言語Lの構文規則を与える
• （言語Lの意味論を与える）
言語Lの型式の構文（規則）を与える
言語Lの型推論規則を与える
– 型推論規則で使われる記法
1. E : T - 式（または文）Eが型Tを持つという命題
2. A - 型環境（前提）と呼ぶ。式の中に現われる変
数や定数が持つ型を与える. A(x) = T は型環境A
においては、変数（または名前）xは型Tを持つ。
3. A |- E : T 型判定(type judgment)と呼ばれ、Aの
もとで式Eが型Tをもつことを表明・主張する。
If-then-else式の型推論規則
E0,E1,E2を式として、
もし E0がbool型の値をもつことが示され
かつ E1の型がTであることが示され
かつ E2の型がTであることが示されたなら
その時 if E0 then E1 else E2は型Tをもつことが示される
これを
形式化して
A |- E0 : bool, A |- E1 : T, A |- E2 : T
-------------------------------------------------------A |- (if E0 then E1 else E2) : T
単相型(monomorphic type)
の推論規則を持つ言語L
LLの型式と記法
Lの型推論規則
型推論の例１
型推論の例２
int>
型推論２（多相型の序）
多相型の型推論に向けて
• 主型(principal type)
• λ計算に型推論を入れる例
・型理論λ→
• 主型の3性質
• 型を持つことの特性
• 多相型の型推論規則を考える上での注意点
主型
•
型多相(type polymorphism, polymorphic type)
を許す言語の型推論を説明する上で重要な
概念。
• 定義：型Tが項ｔの主型であるとは、
次の１）、２）が成立すること。
1. |- ｔ： T が成立。
2. 任意のT1 に対して、|- ｔ：T1 が成立するなら、T
の中の型変数に対する適当な代入σが必ず存在
して、
T1≡Tσ となる。
λ式の型
• 一般のλ式（項）に型を導入する
• 閉じたλ式は一般に関数に対応するから、そ
の型は、関数型である。
• 例えば、 λx.x （恒等関数）の定義域の型をTと
すると、その値域の型はやはりTである。よっ
て、 λx.x ： T → T となることは明らか。
型理論λ→
•
λ→における項：（term、式)を次のように定義す
る：
1. 変数は項である。（x,y,z等の文字を使って表す）
2. ｔ１、ｔ２が項のとき、ｔ１ｔ２も項である。
3. xが変数、ｔが項のとき、λx.ｔは項である。
•
λ→における型式（型のsyntax, 記法）：
1. 変数（ α、β、、、）は型式である。
2. T1,T2が型式のとき、T1→T2も型式である。
項の並び
λ→の型推論規則
1. A |- x : T 但しA(x)＝Tのとき。
2. A |- f : T1→T2 A |- a : T1
--------------------------------A |- f a : T2
3. A + x : T1 |- t : T2
-----------------------A |- λx.t : T1 →T2
複数の型付けと型変数
• K ≡ λxy.x の型は
–
–
–
T1→T2→T1
(T1→T2)→T3→ (T1→T2)
…
• このようにKの型として整合する型は複数あり得る。
一般に型を値とする型変数α、βなどの文字を用いて、
Kの型を K : α→β→α
と表し、このα、βに任意の型を代入すると、Kに整合する
全ての型が得られる。
• すると、α→β→αがKの主型と考えてよい。
λ→の型に関する特徴
•
主型性(principal type properties)ーー Hindley&Seldan
1.
2.
3.
•
項ｔが型をもつなら、ｔは主型を持つ。
項ｔの主型は計算可能である。（計算するアルゴリズムがある。）
主型を計算するO（ｎ）のアルゴリズムが存在する。
ある項が型を持つ（型付け可能である）ことは、その項は以
下の“良い”性質を持つ。
|- t : T （型をもつならば）かつ t -*-> s ならば、 |- s : T
|- t : T ならば（型をもつならば）、どの戦略によっても、簡約は停止し、
t は正規形を持つ。(strong normalizability)
3． |- t : T1 かつ |- s : T2 なら（どちらも型付け可能なら）
t  s か否かを判定する問題は決定可能である。
1.
2.
•
型を持つλ式は限られていて、既に正規形となっている式でも、
型を持たないものもある。
たとえば, λx. xx は型をもたない。（自己適用など）
課題：これ以外に型を持たない正規系をもつ例は？？

Download Report