概要

歴史

型なし言語

l 型なしで構造を処理するプログラミング言語。

l 様々なオブジェクトを処理できる手続きが書ける。

l 一方、わかりにくいバグを見つけなければならなくなる。

例（LISP）：整数アトムにCDRを作用させる。

型付言語

l 手続きの型指定により上記のようなスタイルは排除される（ALGOL68）。

l 手続きの型指定が曖昧な言語では上述のような柔軟性を不完全ながら利用可（ALGOL60）。

目的

表 1：多態（Polymorphism）

universal	パラメタ付き型（parametric）
	包含（inclusion）、継承
adhoc	多重定義（overloading）
	型強制（coercion）

（この分類はCaradelli&Wegner[1985]、紹介論文中ではparametricとadhocについてのみ触れていて、型強制は名前の「多重定義」と考えられている。）

l 主にparametricなpolymorphismを扱う。

l 上記の型なし言語のような型に関する柔軟性とプログラムの堅牢性の両立。

l 理論だけでなく実用性もある。

例：MLの型検査の実装

手法

l コンパイル時型検査：　コンパイル時に型を調べる。
→実行効率のため

l 型推論：　多くの自明でないプログラムにおいて、全く型を明示しなくても文脈から推論できる。（しかし、ユーザー定義の型をその型の演算と共に定義する場合は除く。）
→変数宣言や引数の型を定義するのは別の問題。＋型推論は型を明示した型検査と比しても十分簡潔

l 多態主導：　他では多態手続きの定義に型パラメータを利用するが、ここでは多態な基本演算（代入、関数呼び出し、対や組の作成、リスト処理演算子）を利用して自然に定義する。
基本演算の持つ型制約と変数の宣言/使用からプログラムのフレーズの型を決定。
例：　手続き定義は多態だが、呼び出された際の引数の型と結果の型は文脈から単態に定まる。

以上は命令型言語にも文法的には適用可能だと考えられるし、命令型でない部分言語にも）

概要

l MLコードによる型推論の例

Ø 例1：　map関数

Ø 例2：　タグつけ

l 概念の定義

Ø well typing（正しい型付け）

Ø Semantic Soundness定理

l 型付けアルゴリズムの提示

Ø アルゴリズムW

Ø Syntactic Soundness定理（アルゴリズムWの正しさを保証する）

Ø Wを模倣する改良型アルゴリズムG

l 代入を扱うためのSemantic Soundness定理の拡張

MLコードによる型推論の例

型についての連立方程式を解くと考える。

例1：　map関数

定義

letrec map(f,m) = if null(m) then nil

else cons (f (hd (m)), map (f, tl (m))

期待される型

((α→β)×α list)→β list

αとβは型変数

利用されている演算の型の定義

null: α list→bool

nil: α list

hd: α list→α

tl: α list→α list

cons: (α × α list)→ α list

αは型変数

型の連立方程式

利用している演算の定義から：

σ_null=τ₁list→bool

σ_nil=τ₂list

σ_hd=τ₃list→τ₃

σ_tl=τ₄list→τ₄list

σ_cons=(τ₅×τ₅list)→τ₅list

ここで関数定義から：

σ_map=σ_t×σ_m→ρ₁(関数mapの仮引数から)

σ_null=σ_m→bool（リスト演算nullの具体化）

σ_hd=σ_m→ρ₂（リスト演算hdの具体化）

σ_tl=σ_m→ρ₃（リスト演算tlの具体化）

σ_f=ρ₂→ρ₄（関数f）

σ_map=σ_t×ρ₃→ρ₅（関数mapの再帰呼び出し）

σ_cons=ρ₄×ρ₅→ρ₆（consの具体化）

ρ₁=σ_null=ρ₆（if文の性質）

以上をRobinsonのUnificationアルゴリズムによって解くと

σmap=(γ→δ)×γlist→δlist

が得られる。

ｍapの具体化

以下のような変数と関数があるとき、

tokl: tok list

length: tok→int

sqroot: int→real

以下の式に現われる2つのmapは：

map(sqroot, map(length,tokl))

以下のように具体化される：

((tok→int)×tok list)→int list

((int→real)×int list)→real list

それぞれの中で具体化されている定義も同様：

例　α list→bool ：

tok list→bool,、int list→bool

l 複数回具体化される関数はそれぞれ違う型（仮引数と返値）を持ち得る。

l 再帰定義の場合は同一の型を持つ。

l 具体化に伴ってコンパイラは具体的な定義（コード）を生成する。⇒ユーザーは概念的には同一のものとしてmapを見られる。

例2：　タグ付け関数

問題

(b,c)→((a,b),(a,c))という関数を定義する。

定義1

let tagpair(a)=λ(b,c).((a,b),(b,c))

定義1から得られる型

例1と同様にして：

α→(β×γ→(α×β)×(α×γ))　・・・(*)

と型がつく。

定義2

型：　#: (α→β)×(γ→δ)→((α×γ)→(β→δ))

機能：　(f#g)(a,c)=(f(a),g(c))

と

型：　pair: α→(β→α×β)

機能：　pair(a)=λx.(a,x)

という演算を利用して

let tagpair = λa.(let tag = pair(a) in tag#tag)

定義２から得られる型

α→(β×γ→(α₁×β)×(α₂×γ))　・・・(**)

これは制約が緩過ぎる。

定義3

let tagpair = λa.pair(a)#pair(a)

この定義ならば(*)と同じになる。

l 問題はletによる局所的な束縛とλによる束縛の競合。

解決策

let x=e in e’と(λx.e’)eのsemanticsを同一視する。

概念の定義

サンプル言語Exp

関係のない問題を取り除いた概念説明用の簡易言語

文法

e ::= x | (ee’) | if e then e’ else e’’

| λx.e | fix x.e | let x=e in e’

表 2：式の定義

x	変数
(ee’)	適用(関数eに引数e’を渡して呼び出す)
if e then e’ else e’’	if文式の真偽であるいはを値とする
λx.e	λ抽象、式eで定義される関数本体という値の定義
fix x.e	最小不動点
let x=e in e’	式e’中の変数xを式eに束縛

l 以下d,e,f及び、これに添え字やプライムを付加したもので、この文法で定義される式を表す。

概要

歴史