型推論３（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定義)の本体に現われる変数（名前）の型推論規則を区別する必要がありそうである。 λ抽象の場合、本体中のλ変数である変数の複数の出現は同じ値･型としてinstantiateされる。 let定義で定義される名前は、let式の本体では異なる出現は異なる値・型をinstantiateすることができる。 型推論において上の１，２を区別するために、いくつかの概念を導入する（Robin Milner)。

総称型と型スキーマ 総称型変数(generic type variable) 型スキーマ(shallow types) 同じ型変数で、異なる出現で異なる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の型推論の特徴 多相型を持ち、それはshallow typeである。 型推論アルゴリズムは決定可能である。 　　　　　　　　　　　　　　　　　　　　　決定可能でなくなる。 fix ( letrec) があるので、MLは全ての部分帰納的関数を表現できる。このために型をもつ全てのプログラムが停止するわけではない。（cf. λ→において型をもつλ式は強正規化可能であった。） 課題：λ→の枠組みで不動点演算子が型付けできるか？？

μMLの型推論システム１

μMLの型推論システム２

μMLの型推論システム３ 　αはτ’に出現する全ての型変数のうち、前提Aにも現われないもの。

let-polymorphismの推論例

課題 let f = λx.x in f f の型を求めよ。 （λf. f f )(λx.x)の型付けを試みよ。 　　　証明せよ。

型推論アルゴリズム

Unification(1) Most general unifier

Unification(2)

推論アルゴリズムの導出

推論手続きWのアイデア

推論手続きWのアイデア（２）

μMLの型推論アルゴリズム