型理論の初歩 2007 fall.

Slides:



Advertisements
Similar presentations
ソフトウェア工学 理工学部 情報システム工学科 新田直也. 演習問題 1 の解答例  入庫処理の DFD 酒屋の在庫問題の DFD( 入庫処理 ) 更新情報 在庫ファイル 更新処理 倉庫係 在庫不足リスト 在庫ファイル 出庫指示書 新規出庫 判定 出庫指示書 作成処理 出庫依頼 積荷票.
Advertisements

ソフトウェア工学 知能情報学部 新田直也. オブジェクト指向パラダイムと は  オブジェクト指向言語の発展に伴って形成され てきたソフトウェア開発上の概念.オブジェク ト指向分析,オブジェクト指向設計など,プロ グラミング以外の工程でも用いられる.  ソフトウェアを処理や関数ではなくオブジェク.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
プログラミング演習II 2004年11月 30日(第6回) 理学部数学科・木村巌.
プログラミング言語としてのR 情報知能学科 白井 英俊.
オブジェクト指向プログラミング(4) 静的分析(2)
ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話
クラスその2∽(アドバンス)∽ 福岡工業大学  梶原 大慈       .
Javaのための暗黙的に型定義される構造体
プログラミングパラダイム さまざまな計算のモデルにもとづく、 プログラミングの方法論 手続き型 関数型 オブジェクト指向 代数 幾何.
アルゴリズムとデータ構造1 2007年6月12日
地理情報システム論 第3回 コンピュータシステムおける データ表現(1)
プログラミング言語論 第6回 型 情報工学科 篠埜 功.
第2回:Javaの変数と型の宣言 プログラミングII 2007年10月2日.
オブジェクト指向プログラミング(2) OOPの三大要素 「クラス」「ポリモーフィズム」「継承」
アルゴリズムとデータ構造 2011年6月13日
条件式 (Conditional Expressions)
プログラミング言語論 第10回 オブジェクト指向 情報工学科 篠埜 功.
2006/11/16 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎

オブジェクト指向 プログラミング 第一回 知能情報学部 新田直也.
2007/1/11 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
プログラミング言語論 第12回 関数型プログラミング 情報工学科 篠埜 功.
論文紹介: A Second Look at Overloading
プログラミング言語論 第2回 情報工学科 篠埜 功.
独習JAVA 6.8 コンストラクタの修飾子 6.9 メソッドの修飾子 6.10 ObjectクラスとClassクラス 11月28日(金)
静的型付きオブジェクト指向言語 のための 暗黙的に型定義されるレコード
暗黙的に型付けされる構造体の Java言語への導入
プログラミング言語入門.
お仕事にまったく役にたたない内容のコードレビューやりたいと思います。
プログラミング言語論 第13回 オブジェクト指向 情報工学科 篠埜 功.
国立情報学研究所 ソフトウェア研究系 助教授/
 型推論1(単相型) 2007.
オブジェクト指向言語論 第八回 知能情報学部 新田直也.
第1章 実世界のモデル化と形式化 3.地物インスタンスの表現
フロントエンドとバックエンドのインターフェース
 型推論3(MLの多相型).
プログラミング言語論 第十三回 理工学部 情報システム工学科 新田直也.
ソフトウェア工学 知能情報学部 新田直也.
プログラミング言語論 第十一回 理工学部 情報システム工学科 新田直也.
アルゴリズムとデータ構造 2012年6月11日
国立情報学研究所 ソフトウェア研究系 助教授/
PROGRAMMING IN HASKELL
アルゴリズムとデータ構造1 2009年6月15日
オブジェクト指向言語論 第五回 知能情報学部 新田直也.
プログラム分散化のための アスペクト指向言語
プログラミング言語論 第2回 篠埜 功.
PROGRAMMING IN HASKELL
Eijiro Sumii and Naoki Kobayashi University of Tokyo
第6回放送授業.
18. Case Study : Imperative Objects
SMP/マルチコアに対応した 型付きアセンブリ言語
オブジェクト指向言語論 第九回 知能情報学部 新田直也.
オブジェクト指向言語論 第二回 知能情報学部 新田直也.
アルゴリズムとデータ構造 2010年6月17日
ソフトウェア工学 知能情報学部 新田直也.
オブジェクト指向言語論 第一回 知能情報学部 新田直也.
プログラミング言語論 第九回 理工学部 情報システム工学科 新田直也.
Javaとは Javaとはオブジェクト指向言語でJava VM(Java仮想マシン)と呼ばれるプログラム上で動作します。
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
オブジェクト指向言語論 第七回 知能情報学部 新田直也.
オブジェクト指向言語における セキュリティ解析アルゴリズムの提案と実現
プログラミング言語論 第九回 理工学部 情報システム工学科 新田直也.
オブジェクト指向言語論 第七回 知能情報学部 新田直也.
情報処理Ⅱ 2005年11月25日(金).
全体ミーティング(9/15) 村田雅之.
オブジェクト指向言語論 第九回 知能情報学部 新田直也.
Static Enforcement of Security with Types
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
Presentation transcript:

 型理論の初歩 2007 fall

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

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

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

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

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

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

ADTの要点2 4. 抽象データ型を、一般に定義すると: データ・対象の集合 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 によって特徴つけられる。

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

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

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

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

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

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

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(β)

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