型システム

提供: miniwiki
移動先:案内、検索

型システム（英: type system）とは、プログラミング言語において、その式などの部分が持つ値を、その種類（型(type)、データ型も参照）に沿って分類し、プログラムが正しく振る舞うこと、といった性質について保証する手法である。型システムは、型理論に基づいており、プログラミング言語の理論において最も確立された軽量形式手法である[1]。

定義

型

プログラミング言語はさまざまな値を扱う。三角関数は浮動小数点数を引数にとり浮動小数点数を返す。先頭の文字を大文字にする関数は文字列を引数にとり文字列を返す。ユーザーからの入力を数値として扱うためには、文字列を解釈して数値を返す関数が必要である。ここで、3.14 や "hoge" といった値について「浮動小数点数」や「文字列」といった種類に分類して扱っているが、同じ種類の値であれば同じ操作が可能である。この「値の種類」が型である。

型検査

プログラムにおけるエラーはさまざまだが、型に基づく一連のエラーがある。単純な例としては、浮動小数点数を表現しているワードを（一般的なコンピュータのハードウェアでは、メモリ上のワードとしては区別がつかないため）整数型として扱ってしまう、といったようなものである。この例では 0 と +0.0 のような特別な場合を除いてたいていの場合は得られる結果は無意味であり、より複雑な構造を持った値の場合は構造を壊して不正にしてしまうかもしれない。このような異常をプログラムが起こさないことを検査するのが型検査である。

静的型付けと動的型付け

"「静的型付け」および「動的型付け」"

プログラムを実行前に型検査を行うのが静的な型付け、静的型付けであり、プログラムを実行しながら型検査を行うのが動的な型付け、動的型付けである。

Javaは一般に静的型付け（静的型付き言語）であるが、ダウンキャストは明示する必要があり実行時に型検査を受ける。Common Lispは一般に動的型付け（動的型付き言語）だが、type specifierという静的に型を指定する文法も持っている。といったように、ある程度は混在している言語もある。さらに、静的検査が行われるタイミングについても、コンパイル時の他リンク時やインタプリタのソースコード読み込み時といった場合もありえるため、簡単に見た目では分類できないこともある。

型なし

型付けを更に厳密に定義した区分として型なし（英: untyped）という区分が存在する[2]。代表的な言語はSmalltalkで高速化のため処理系依存で実行時に型検査することがあるものの言語的には型検査がなく動的型付け言語のように文字列に割り算をするといった不正な操作をしても処理系が型検査して停止する事は無い。型なしの言語では処理系が型検査をしない代わり、ライブラリーで例外を投げて停止する。例えばSmalltalkではオブジェクトに対し対応するメソッドが存在しないメッセージを投げると最終的にクラスごとに定義した#doesNotUnderstand:メソッドに至る。このメソッドが例外を投げるようになっていればば停止するがそうでなければ停止することなく走り続ける。 型なしの言語は最適化がしづらい反面、オブジェクトの操作を処理系に制限されないため使用者が後から自由にオブジェクトの操作を追加できる利点がある。

安全性

型にまつわるものに限らず一般に、プログラムが言語で定義していない状態（たとえばバッファオーバーランなどによる）や、言語仕様で「未定義」とされている状態（たとえばC言語の標準では、そういった「未定義」の場合が決められている）にならない、という性質。プログラムのエラーを（エラーが原因の異常動作によるセグメンテーション違反などによってではなく）ランタイムやインタプリタが検出して異常終了するような場合も「安全」の側に含まれる。型にまつわる安全性が型安全性である。

型安全でない例としては、C言語などにおいて、32または64ビットの整数型と浮動小数点数型は暗黙的な型変換が行われることがある。このときに得られる値は主に処理系に依存する（丸め処理を行う関数は別途用意されているが、暗黙的な型変換では利用されない）。そのため、この型同士で暗黙的な型変換を利用してしまうと期待はずれの結果になる。典型的な例として、printfなどで、丸め処理をせずに表示すると生じる。また、for文で浮動小数点数型をカウントに用いる場合でも、ループ回数が変わってくることがある。

強い型付けと弱い型付け

型検査によって型安全性があるような型付けが強い型付け、無いものが弱い型付けである。たとえばMLは静的で強い型付け、Cは静的で弱い型付けである。強い型付けの利点としては、型検査時の決定的な型保証による実行時の型不一致による不正動作の抑制がある。型検査時に型の機能を決定させているため、実行時の型変更は許されないと同時に予期しない動作も起こせない。一方で、弱い型付けの利点としては、Cの構造体で見られる様な、型の一部の機能が一致していれば厳密には型が不一致であってもその機能が扱えるというものがある。実行時の型変更を認めることにより、柔軟な扱いを可能とする。

プログラムの安全性の定義については論者による議論もある所であり、またバッファオーバーランのように、型検査でプログラムの全ての安全性を保証できるわけでもないが、型システムによる大きな利点があることは確かである。

明示的な型付けと暗黙的な型付け

Cのように型を直接具体的に書く（必要がある）型付けが明示的（explicit）な型付け、Haskellのように変数の使われかたなどから型推論により型付けが行われるのが暗黙的（implicit）な型付けである。

議論

静的型付けと動的型付け

静的型付き言語はいわゆるコンパイラ言語に、動的型付き言語はいわゆる動的プログラミング言語によくみられる。

型検査がどのように働くのかを見るために、次の擬似コードを考える。 

var x;
x := 5;
x := "hi";

この例では、1行目でxという名の変数を宣言し、2行目でxに整数5を代入し、3行目でxに文字列"hi"を代入している。ほとんどの静的型付けの処理系ではこのようなコードは不正（型エラー）となる。なぜなら2行目と3行目でxに一貫性のない型の値を代入しているからである。

対照的に動的型付けの処理系では、型は変数ではなく値に付けられるので、上のようなコードが実行できる。動的型付けの処理系は間違った文や式を実行したときに、値の誤用に関するエラーを型エラーとして捕捉する。つまり、動的型付けはエラーをプログラムの実行中に捕捉する。動的型付けの典型的な実装ではプログラム中のすべての値が型情報を持ち、演算に値を使う前に型情報を確かめる。例を挙げる。 

var x := 5;
var y := "hi";
var z := x + y;

このコードでは、1行目でxを値5で束縛し、2行目でyを値"hi"で束縛し、3行目でxとyを足そうとしている。動的型付き言語ではxを束縛した値は(整数, 5)というペアとして表すことができ、yを束縛した値は(文字列, "hi")というペアで表すことができる。プログラムが3行目を実行しようとしたとき、処理系は整数と文字列という型情報を検査し、もし演算+（加算）がその2つの型について定義されていなかったら、エラーを出す。

プログラミング言語の中には、静的に型検査されないコードをプログラマが書けてしまう「バックドア」を持つものもある。例として、JavaやC風の言語には「キャスト」がある。

プログラミング言語が静的型付けをもつことは必ずしも動的型付けをもたないことを意味するわけではない。例えばJavaは静的型付けを採用しているが、処理によっては動的な型情報の取得を必要とするものもあり、それらは動的型付けの一形態とみなせる。静的型付けと動的型付けの違いについては様々な議論がある。

性質

最適化
静的な型検査によってコンパイラは最適化に有用な情報を得ることがある。例えばある型の値が4の倍数のアドレスに配置されることが保証されていれば、コンパイラはより効率の良いマシン命令を選択できる。
可読性
より表現力の高い型システムでは型はプログラマの意図を説明することができるので、ドキュメントの役割を果たすこともある。例としてタイムスタンプが整数の派生型である環境において、プログラマが単なる整数ではなくタイムスタンプを返す関数を宣言すると、その型情報が関数の意味を記述していることになる。
抽象化またはモジュール化
型によってプログラマは低レベルでの実装に煩わされずにより高レベルで考えることができるようになる。例えば文字列型によってプログラマは文字列を文字列として、単なるバイトの列ではないものとして考えることができる。また型によってプログラマは2つのサブシステム間のインタフェースを表現することができる。これはサブシステムの相互運用性に必要な定義を局所化し、それらのサブシステムが通信する際に起きる矛盾を防止する。

バリエーション

典型的には、プログラム中ではすべての値には1つの特定の型が付けられる（1つの型が複数の派生型を持つ場合でも）。オブジェクトやモジュール、通信路、依存関係、及び型自身にさえ型が付けられることもある。例を挙げると

データ型 
値の型
クラス 
オブジェクトの型
カインド 
型の型

などがある。

プログラミング言語ごとにある型システムは型付けされたプログラムがどのようにふるまい得るかを規定し、その規則から外れたふるまいを不正であると判定する。型システムより粒度の小さいコントロールはエフェクトシステムが提供する。

トレードオフ

静的型付けか動的型付けかの選択はいくつかのトレードオフを必要とする。

静的型付けは型エラーをコンパイル時にある程度確実に発見する。よって最終的なプログラムの信頼性を上げるはずである。しかしながら、型エラーがどれほど犯しやすい間違いなのか、その内の何割が静的型付けで検出できるのか、という点についてプログラマの意見は割れている。静的型付けの支持者は型検査されたプログラムの方が信頼性が高いと信じており、それに対して動的型付けの支持者は実際に流通しているソフトウェアの信頼性では大差ない点を指摘している。

静的型付けは大抵、より高速に実行可能なコンパイル済みコードを生成する。コンパイラが正確なデータ型を知っていれば、最適化されたコードを生成できる。さらに、静的型付き言語のコンパイラではショートカットをみつけるのもより簡単になる。この理由からCommon Lispなどのいくつかの動的型付き言語では随意で型宣言ができるようになっている。最適化のための型付けは静的型付けの影響で普及した。

対照的に、動的型付けのほうがコンパイラやインタプリタの動作が高速になることがある。動的型付けの言語ではソースコードが変更されてもやり直すべき解析が少ないためである。これは「編集-コンパイル-テスト-デバッグ」というサイクルの時間を減らす。

型推論のない静的型付き言語（Javaなど）ではプログラマがメソッドや関数の型を宣言しなければならない。これはプログラムの追加的なドキュメントとして機能することがあり、コンパイラによってコードと同期させることが強制される。しかし型宣言のない静的型付き言語もあるので、これは静的型付けのというよりは型宣言の報酬である。

動的型付けはいくつかの静的型付けでは不正となり実現できない仕組みを可能にする。例えばデータをコードとして実行するeval関数である。さらに動的型付けでは、具体的なデータ構造の代わりに文字列を暫定的に用いることなどがやりやすく、プロトタイピングとの相性も良い。

動的型付き言語のメタプログラミング機能はより強力で使いやすいことが多い。例を挙げると、C++のテンプレートはRubyやPythonでの等価なコードより、書くのが煩わしい。またイントロスペクションのような、より高度な実行時の仕組みを静的型付き言語で使うのは、さらに困難になることが多い。

ポリモーフィズムと型

"「ポリモーフィズム」"

ポリモーフィズム（多相）という語は、コード（具体的には関数やクラス）が複数の型の値に基づいて動作できること、または同じデータ構造の異なるインスタンスが異なった型の要素を持てることを指す。型システムによってはコードの再利用性を改善するためにポリモーフィズムを持つものもある。ポリモーフィズムのある言語ではプログラマはリストや連想配列のようなデータ構造を使用される要素の型ごとにではなく、単に一度だけ実装すればよい。この理由から計算機科学ではこの種のポリモーフィズムの利用はジェネリックプログラミングと呼ばれることがある。ポリモーフィズムの型理論における基礎は抽象化やモジュール、また（場合によっては）派生型についての研究と密接な関連がある。

ダック・タイピング

プログラミング環境によっては、2つのオブジェクトの間に全く関係がなくともそれらが同じ型を持つことがある。例としてはC++のポインタとiteratorの双対性が挙げられる。両方とも * 演算が定義されているが、全く別のメカニズムによって実装されている。

このテクニックは「ダック・タイピング（Duck Typing）」と呼ばれる。由来は次の警句である。

"If it waddles like a duck, and quacks like a duck, it's a duck!"

明示的または暗黙的な型の宣言と型推論

"「型推論」"

多くの静的な型システム（例えば C や Java）は型宣言を必要とし、プログラマはすべての変数に特定の型を明示的に関連付けなければならない。そうでないもの（例えば Haskell）は型推論を行い、コンパイラはプログラマの変数に対する扱いから変数の型についての結論を引き出す。例として、x と y を足す関数 f(x, y) を仮定すると、コンパイラは加算は数値のみに定義されているので x と y は共に数値であると推論できる。ゆえにプログラム中で f の引数として数値でない型（文字列やリストなど）を取って呼び出すとエラーを報告する。

コード中の数値や文字列のリテラルおよび式は型を暗示する。例えば、式 3.14 はおそらく浮動小数点数を暗示し、式 1, 2, 3 はおそらく整数のリスト（主に配列）を暗示する。

互換性（等価性と派生型）

静的型付き言語の型検査では、すべての式の型がその式が現れた文脈で期待される型と一貫しているか、検証しなければならない。たとえば、x := eという代入文では式eの推論される型は変数xの宣言型または推論型と一貫していなければならない。この一貫性の概念を互換性といい、プログラミング言語ごとに固有のものである。

明らかなように、eとxの型が同一でかつその型への代入操作が許可されているなら、これは正当な式である。したがって最も単純な型システムでは、2つの型が互換であるかどうかは2つの型が同一である（または等価である）かどうか（等価性）という単純な問題に置き換えることができる。別の言語では2つの式が同じ型を持つと理解されるのに別の基準を採用している。これら、型の同一性理論は非常に多岐にわたっており、2つの極端な例は structural typing と nominative typing である。structural typing とは同じ外部構造（インタフェース、特に暗黙的なもの）を持つ値を同じ型であるとするもので、nominative typing とは型宣言の構文からのみ型の同一性を判定する（型が同じ「名前」を持たなければならない）ものである。

派生型のある言語では互換性の関係はより複雑なものとなる。型Aが型Bの派生型であるとすると、A型の値はB型の値が必要とされる文脈で使用することができる。しかし逆は真ではない。等価性と同様に派生型の関係はプログラミング言語によって異なった方法で定義され、多くのバリエーションが存在しうる。パラメータ付けされたまたはアドホックなポリモーフィズムを持つ言語の存在は型の互換性に何らかの意味を持つのかもしれない。

論争

静的および強い型付けの支持者と動的および自由な型付けの支持者の間では衝突が度々おきる。前者のグループは厳密な型付けの使用によって、処理系がより多くのエラーを問題が大きくなる前に発見できるようになると主張している。後者のグループはより気軽な型付けによってコードはよりシンプルなものになり、そのようなコードは解析しやすいとされるので、エラーは減少すると主張している。型推論がある言語では型を手で宣言する必要はほとんどないので、強い型付けに伴う開発のオーバーヘッドは低減される。

個人がどのグループに分かれるかは、開発しているソフトウェアの種類やチームのメンバーの能力、他のシステムとの対話性の度合い、開発チームの規模などに依ることが多い。少人数で小回りのきくプロジェクトには気軽な型付けがより合い、フォーマルで大人数で仕事が分断されている（プログラマ、アナリスト、テスト部隊、など）プロジェクトは厳密な型付けのほうがうまくいくことが多い、と結論づける者もいる。

脚注

  1. ↑ 『型システム入門』 p. 1
  2. ↑ http://web.cecs.pdx.edu/~harry/musings/SmalltalkOverview.html

参考資料

関連項目

テンプレート:データ型



「http:///http:///mymemo.xyz/mymemo.xyz/wiki/index.php?title=型システム&oldid=254947」から取得