Document

型推論３（MLの多相型）
MLの型多相
• ML言語設計では、任意の式に多相を許すわけ
ではない。
• let-polymorphism
– let pr = λx. Print(x) in…pr(3)…pr(x=3)…
– let <名前> = <式1> in <式2>
<式２>の中で使われる<名前>の複数の出現に
ついてのみ異なる型を持ってよい。この形の制限され
た
型多相のみが許されている。
MLの多相型の形式化に向けて
• ナイーブなアプローチ： λ→の型式の中に導入したような
“型変数”をもちこみ、次のような単純な推論規則を付加する。
A |- E : T
------------- （＊）
A |- E : T’ 但し T’はT中の型変数に代入を施したインスタンス
• この方式では次の２つの問題が生じる：
問題点（1） λx. [succ x not x] ：α -> (int x bool)
が証明されてしまう。
（課題：ナイーブなアプローチでこれを証明せよ。）この証明の結
果は、我々の“λ抽象”に対する直感から外れたものである。即
ちf x =＜関数本体＞に現われるxは全て同じ値をもつ、ゆえに
同じ型を持つはず、という直感に反する！！！
問題点（２） MLでは、いわゆる let-polymorphismという制限され
た形の多相型の使用のみが言語設計上許されている。これを
表すのに上で示した簡単な推論規則（＊）では対処できない。即
ち：
let id = λx.x in [id(3), id(true)] におけるidはlet内で定義
されたもので、型多相な関数として、この定義が正しく型づけが
できるようにしたい。
( letの定義では id : α→α,
本体の中では id : int  int, id : bool  bool )
二つの推論規則の導入
•
以上の考察から、λ抽象する変数（名前）と、局
所定義(let定義)の本体に現われる変数（名前）
の型推論規則を区別する必要がありそうである。
1. λ抽象の場合、本体中のλ変数である変数の複数の
出現は同じ値･型としてinstantiateされる。
2. let定義で定義される名前は、let式の本体では異なる
出現は異なる値・型をinstantiateすることができる。
•
型推論において上の１，２を区別するために、い
くつかの概念を導入する（Robin Milner)。
総称型と型スキーマ
• 総称型変数(generic type variable)
– 同じ型変数で、異なる出現で異なるinstantiationする
ことができるものをいう。
– 同じ型変数で、全ての出現に対して、常に同じ
instantiationしか許されないものを非総称型変数
（non-generic type variable）とよぶ。
• 型スキーマ(shallow types)
– 型式Tが型変数α1, … ,αnを含むことがあり得て、
かつその中にが現われないとき、
α1, …, αn T の形をした型式を
型スキームとよぶ。またshallow type とも呼ばれる。
（ α. α →α） → （ α. α →α）
非例
型スキームのinstantiation/特化の規則
• 型スキームをinstantiateした結果の型も、
型スキームでなければならない。すなわち、
shallow type の特化したものはshallow type
でなければならない。
– α. (α →α）のαにintを代入すると int → intとなりこれは
shallow typeであるのでこの代入は型スキームの特化として
OKである。
– α. (α →α）のαに β.β→intを代入して得られるとこの
（ β.β→ int） → （ β.β→ int）は型スキーム/shallow type
でないので、この代入は型スキームのinstantiationではない。
Generic Instance
•
より形式的な定義：
S, S’ をtype schemeとする。S’がSのgeneric instanceとは S ＞ S’
と書き、次の条件を満たす。
– S’はSの限量化されている幾つかあるいは全ての型変数に
代入を行い、さらに必要があれば、代入の結果、もとのSで
自由であった型変数以外のものを限量化して得られる型ス
キームである。
– More precisely, S = α1… αm.τ
S’ = β1… βn.τ’
•
•
–
τ’= [τi/αi]τ for some τ1,…τm’ (m’ ≦ m)
βi はSで自由でない。
例： α. (β →α）＞ γ.(β→（βｘγ）） OK
α. (β →α）＞ β. γ.(β→（βｘγ））
NG
MLについて
•
•
Meta Languageの略。‘７０はじめに、R.Milnerが基本
設計。LCF(Language for Computable Logic)という表
示的意味論にもとづく、computable functionに関する
verification systemのために証明戦略等を記述するメ
タ言語をもとにして、発展した。
特徴
–
–
–
–
基本的に関数型言語
非明示的な型多相言語
実用的言語
全ての単純な構文単位がterm(項/式）とみなせる。
・ SML（Standard ML): 抽象データ型（ADT)と
“module”機能を持つ。
MLの型推論の特徴
1. 多相型を持ち、それはshallow typeである。
2. 型推論アルゴリズムは決定可能である。
shallow typeより表現力の強い多相型を許すと
決定可能でなくなる。
fix ( letrec) があるので、MLは全ての部分帰納的関
数を表現できる。このために型をもつ全てのプログラ
ムが停止するわけではない。（cf. λ→において型をも
つλ式は強正規化可能であった。）
4. 課題：λ→の枠組みで不動点演算子が型付けできる
か？？
3.
μMLの型推論システム１
μMLの型推論システム２
μMLの型推論システム３
αはτ’に出現する全ての
型変数のうち、前提Aにも
現われないもの。
let-polymorphismの推論例
課題
1. let f = λx.x in f f の型を求めよ。
2. （λf. f f )(λx.x)の型付けを試みよ。
3. |- let f ＝λx.x in f f : α→α という型判定を
証明せよ。
型推論アルゴリズム
Unification(1)
Most general unifier
Unification(2)
推論アルゴリズムの導出
推論手続きWのアイデア
推論手続きWのアイデア（２）
μMLの型推論アルゴリズム

Download Report