型理論の初歩 2007 fall.

Presentation on theme: "　型理論の初歩 2007 fall."— Presentation transcript:

1 　型理論の初歩 2007 fall

2 型とは 「型」とは、一般に値の集合（見方に2つあり） 型の効用： プログラムの表現の立場： プログラム中の式/文が取れる値に関する制約
プログラムの表現の立場：　プログラム中の式/文が取れる値に関する制約 対象領域に登場する実体のモデル化の表現（クラス、、、） 型の効用： モデル化と分類をプログラマに明確に意識させる。 コンパイラによって型検査ができ、コンパイル時に型エラーの検知範囲を拡大できる。　（実行時にも同様に可能） 型情報を介して、インターフェースと実現の分離を可能にする。 型情報を用いたコードの分析や最適化が可能になる。 型概念は発展し続けており、プログラムにかんする様々な解析を可能にしつつある。

3 型概念の発展 基本データ型： 数、真偽値、文字、、、 → ビット列の符号化/再生化が基本的な考え。
基本データ型：　数、真偽値、文字、、、 →　ビット列の符号化/再生化が基本的な考え。 2. 構造データ型：　配列、構造、レコード（直積）、 　　 　　　　　　　　　　　union/variant（直和） 3. 抽象データ型：　プログラマの意図に従って強い型付 　　　　　　　　け、型検査ができる言語系に備わる。 4. 型なし：　型無しλ計算、Lisp, Scheme 動的型(dynamic type):　実行時に始めて型がきまる。 型宣言の省略:　型推論 型多相：　コードの再利用性の向上、 　　　　　一般的なコード記述 8. 部分型：　オブジェクト指向の継承やコードに再利用

4 関連する諸概念 型安全：プログラム実行中に型エラーが生じない 静的な型付け: （全ての）式の型がコンパイル時に確定すること
静的言語：　プログラム中の全ての式の型がコンパイ 　　ル時に確定できる言語 強く型付けされた(strongly typed)言語: 　　　型安全なプログラムだけを実行させる処理系を持つ 「静的に型付け可能」　＝＞　「強く型付けである」 　「強く型付けである」 ＝／＝＞ 「静的に型付け可能」

5 諸概念の関係 型システムが強過ぎて、型安全なプログラムの数が非常に少ない、あるいは空集合にさえなってしまうこともある。
　　　　　型システムが強過ぎて、型安全なプログラムの数が非常に少ない、あるいは空集合にさえなってしまうこともある。 プログラム プログラム 型安全 弱い型付け 強い型付け 型安全 図3.1 型安全性と型付けの強弱

6 抽象データ型(Abstract Data Type)
ADTの定義・記述を中心的なモジュールとしてプログラムを設計することを念頭に置いた言語をADT言語と呼ぶ：　例として、CLU(Liskov’７5),　Modula, ADAなどがある。 いわゆる構造的プログラミング(structured programming)を奨励するための言語でもあった。 MLなどの関数型言語の多くは、基本的にADTの定義機構を持っている。型概念を明確にした歴史的意義も 　持つ。 オブジェクト指向への一歩手前にある言語。 基本データ型や構造データ型より上にある、ユーザがそえを定義する型概念(user defined types)。(より上の型概念）。

7 ADTの要点１ 演算・操作: 特定の性質や制約を持ったデータを対象として使われることを想定して定義・設計する。
演算・操作:　特定の性質や制約を持ったデータを対象として使われることを想定して定義・設計する。 データ・対象：　特定の機能や、特定の性質持った演算・操作に作用されることを、想定されている。 １，２から、データ・対象とそれに作用する演算を分離して定義することは、あまり意味がない。 　　(代数的構造　<集合, {op1, op2, …, opn}>　のようなもの。）

8 ADTの要点２ ４. 抽象データ型を、一般に定義すると： データ・対象の集合 D 操作・演算の集合 OP
OPに属する演算のみがDを生成・操作する手段 Dの外部から見た挙動はOPの中の演算同士の関係だけで、完全に特徴つけられる。　　　　代数構造 例： stack型　　　　　　　　　　　　　　semantics 　　　 new:  stack isnew?(new) = true push: stack x elmt  stack isnew?(push(s,i)) = false pop: stack  stack top(push(s,i)) = i top: stack  elmt pop(push(s,i)) = s isnew? : stack  bool top(new) = undef interface によって特徴つけられる。

9 ADTの実現(内部表現） ５．たとえばstack型の場合、2つの異なる実現： ６． ADT言語の定義機構は
（１） 　arrayを用いる （２）　<要素、ポインター>の対の連鎖を用いる ６．　ADT言語の定義機構は 　　(1)型データの内部表現の定義、と 　　(2)演算･操作の内部表現に対する操作・プロ　　　　　 グラミングの定義 　　をテキスト上分離せずに記述する。 ２方法

10 ADT実現の失敗例（失敗） 名前 属性 名前 属性 Pascal・CのコンパイラのADTとしての名前表型を定義：
　record　と　pointer で実現する。 　　　　　type symtab = ↑entry: 　　　　　 entry = record name: string 　　　　　attribute: string 　　　　　next: symbtab end ; PascalではADTは実現できない！！ 上の例でわかるように、名前表を名前を指定してその属性 を得る、演算(たとえば、retrieve演算）を用いずにポインタを たどたり、ポインタを勝手に切断してしまうことができる。 Stack型をでセルとポインターの対の連鎖で実現しても、同じことが可能で、 　内部表現の一貫性を保証できない！！ 名前 属性 名前 属性

11 ADTの実現例 a la CLU abstype <ADT名> is <演算１>, …, <演算ｎ>
これが一つのモジュール abstype　<ADT名> is <演算１>, …, <演算ｎ> rep = <型の指定・内部表現> <型定義> ; … ; <型定義>; <演算1定義>; … <演算n定義> ADT(モジュール）の使いかた symtab$enter(<table>,<name>,<attribute>) ←　新しいエントリを挿入 symtab$attirbute(<table>,<name>)　←　<name>のもつ属性を知る。

12 ADT実現の言語機構(要点） 抽象データ型を定義・実現するための構文的な単位が言語に備わり、次の１，２が分離せず記述できる。
内部表現の記述　 操作･演算を実現する手続きや関数が定義できる。 内部データ表現へのアクセスは、１で述べた構文単位になかで定義されている演算・操作に限られる。他の方法でアクセスされることが不可能でることが、言語の意味論に保証されている。(Data Encapsulation) 2から派生することだが、ADTを完全に実現する言語は強く型づけされた言語である。

13 型多相へ LispやSmalltalkのような型無しの言語では、複数の型に対して同一の関数(や手続き)あるいはメソッド適用することが可能である。たとえば、リストの長さを調べる関数lengthは、Lispで対象となるリストの構成要素がどのような型を持っていようが、同じlengthという関数を用いることができる。すなわち、lengthはいわゆる型多相的な関数(type polymorphic function)である。一方、静的に型付けされた言語の多くは、このようなことができない。なぜなら、これらの言語では、要素の型がことなるリストは、異なる型を持つリストとして扱い、互いに区別されなければならず、このため基本的には、異なる型のリストごとに異なるlength関数を用意しなければならない(実際、lengthへの入力パラメタの型が異なれば、length関数自身の型も異なるわけである)。 　一般に、プログラムの文面上に現れる同一の式が複数の型を持つ現象は型多相(type polymorphism)と呼ばれるが、これは当然のことながら、プログラムの再利用性を高める上で著しい効果がある。型多相のこのような利点を保ち、かつ強い型付けや抽象データ型定義機構を保持するようなプログラミング言語の設計が実際に行われている。

14 Type Polymorphism（型多相）
プログラム中の同一の式、文等が複数の型を持つ現象 同一の演算、関数・手続きが複数のデータ型に対して作用することが可能である現象。 分類： ad hoc polymorphism – operator overloading 例えば＋や＝は限定されてはいるが複数の型の作用する演算である。　しかし、言語によって指定された範囲の型に対してしてのみ多相的である。 2. Universal/systematic polymorphism Parametric polymorphism Inclusion (or bounded) polymorphism　←　継承・部分型に関する型多相

15 Parametric Polymorphismの例
関数length：　 list, array, set等に同じ関数が適用できる 関数id： 　任意のデータ型の値に対してそれ自身を返す twice = λf.λx. f (f x) (twice succ) 0  2 ((twice twice) succ) 0  4 但し　succ : num  num twice: ~~  ~~ mapcar f l : (α  β)  list(α) 　list(β)

16 2種類のparametric polymorphismの表現
Explicit --- 多相関数を適用する時、陽に型パラメタを与えることを要請する。 let val id = fun(t: type) fun (a: t) a in … id(int)(3)  3, id(bool)(true)  true 上のように実引の型を与えて用いる。 Implicit --- 型適用、型パラメタを許さない 　let val id = fun(a:α) a あるいは　id ＝ λa.a id(3)  3, id (true)  true 課題：　“Explicit parametric” polymoprhism is more expressive than “implicit” one!!! Think about WHY