型システム

型システムの最新ニュースをまとめて検索！

型システム（type system）とは、プログラミング言語において値や式をデータ型に分類し、型を扱い、またそれらが相互作用する方式を定義する仕様及び実装である。 1つの型は共通の汎用的意味または用途を持つ値の集合1つを表現する。^[1]型システムは言語ごとに非常に異なっているが、おそらく最も大きな違いはその文法および実行時における動作においてである。

コンパイラでは値の記憶効率や値に対する操作アルゴリズムの選定を最適化するために静的型が用いられることがある。例として多くのCコンパイラではfloat型を単精度浮動小数点数のためのIEEE標準にしたがって32ビットで表現する。よって加算、乗算等に各浮動小数点数演算が用いられる。

型の強制の度合いや評価方法は言語の型付け（typing）に影響する。さらに、ポリモーフィズムのある言語では一つの演算がいくつかの具象アルゴリズムに対応付けられる。型理論は型システムを対象とした形式的な研究であるが、実際のプログラミング言語の型システムはコンピュータ・アーキテクチャや言語設計及び処理系の実装の実用上の課題から生まれたものである。

[編集] 基礎

型を割り当てること（「型付け」）によってビットの集まりに意味が与えられる。型は通例、メモリ中の値と変数の両方と関連する。コンピュータではすべての値は単なるビットの集まりなので、ハードウェアはメモリアドレスやオペコード、キャラクタ、整数、浮動小数点数などの基本的なデータの間でさえ何の区別も行わない。型はプログラムとプログラマにそれらのビット列をどのように扱うべきかの情報を与える。

型システムがもたらす主要な機能には以下のようなものがある。

安全性

型の使用によってコンパイラが無意味な、または不正であろうコードを検出することが可能になる。例えば人間は "Hello, World" / 3 という式を見ると、文字列を整数で（通常の感覚では）割ることができないので、不正であると認識できる。強い型付けはさらなる安全性をもたらすが、必ずしも完全な安全性を保証するものではない。

最適化

静的な型検査によってコンパイラは最適化に有用な情報を得ることがある。例えばある型の値が4の倍数のアドレスに配置されることが保証されていれば、コンパイラはより効率の良いマシン命令を使うことができるかもしれない。

可読性

より表現力の高い型システムでは型はプログラマの意図を説明することができるので、ドキュメントの役割を果たすこともある。例としてタイムスタンプが整数の派生型である環境において、プログラマが単なる整数ではなくタイムスタンプを返す関数を宣言すると、その型情報が関数の意味を記述していることになる。

抽象化またはモジュール化

型によってプログラマは低レベルでの実装に煩わされずにより高レベルで考えることができるようになる。例えば文字列型によってプログラマは文字列を文字列として、単なるバイトの列ではないものとして考えることができる。また型によってプログラマは2つのサブシステム間のインタフェースを表現することができる。これはサブシステムの相互運用性に必要な定義を局所化し、それらのサブシステムが通信する際に起きる矛盾を防止する。

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

データ型 

値の型

クラス 

オブジェクトの型

カインド 

型の型

などがある。

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

[編集] 型検査

型による制限を検証し、実施する処理は型検査と呼ばれ、コンパイル時（静的検査）と実行時（動的検査）のどちらかまたは両方のタイミングで行われる。型検査はコンパイラが行う意味解析の一部である。プログラミング言語が型の規則を強く適用するなら、つまり自動的な型変換を情報が失われないものに限定するなら、強く型付けされていると言い、そうでなければ弱く型付けされていると言う。

[編集] 静的な型付けと動的な型付け

詳細は「静的型付け」、「動的型付け」をそれぞれ参照

プログラミング言語で、型検査が実行時の式に関する同値性の検査なしに行われることがあるならば、その言語は静的型付けであるという。 静的型付けされた言語にはコンパイル時と実行時という型検査の2つの段階がある。これに加えてリンク時の段階を持つ処理系も存在する。プログラムのいくつかのモジュールが実行時に判明する他のモジュールの情報なしに個別に型検査されるのなら（分割コンパイル）、その言語にはコンパイル時の型検査が存在する。

プログラミング言語がメタデータに基づく実行時の（動的な）ディスパッチを持つならば、その言語は動的型付けであるという。 動的型付けでは実行パスによって変数が異なった型をもつので、型検査は実行時に行われることが多い。動的型を対象とした静的な型システムは通例、実行パスの概念を明示的に表現して、型がそれに依存することに対応しなければならない。

動的な型付けはスクリプト言語やRAD言語などによくみられる。インタプリタ言語では動的型が採用されることが多く、コンパイラ言語では静的型が採用されることが多い。

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

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は静的型付けを採用しているが、処理によっては動的な型情報の取得を必要とするものもあり、それらは動的型付けの一形態とみなせる。静的型付けと動的型付けの違いについては様々な議論がある。

[編集] トレードオフ

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

静的型付けは型エラーをコンパイル時にある程度確実に発見する。よって最終的なプログラムの信頼性を上げるはずである。しかしながら、型エラーがどれほど犯しやすい間違いなのか、その内の何割が静的型付けで検出できるのか、という点についてプログラマの意見は割れている。静的型付けの支持者は型検査されたプログラムの方が信頼性が高いと信じており、それに対して動的型付けの支持者は実際に流通しているソフトウェアの信頼性では大差ない点を指摘している。 静的型付けの価値は型システムの強度が上がるにつれて高まっていくと考えられる。MLやHaskellなどの強く型付けされた言語の支持者は、プログラム中のデータ型を十分にプログラマが宣言するかコンパイラが推論すれかすれば、ほぼすべてのバグは型エラーとみなせると提案している。^[2]

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

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

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

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

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

[編集] 強い型付けと弱い型付け

強い型付けの定義の1つは、ある処理・演算が間違った型の引数をとることを禁止するというものである。例えばCでは不正なキャストができるが、これは強い型付けが存在しないことを示している。コンパイルが通ってしまうというだけでなく、実行時にも許されてしまうからである。これはコンパクトで高速なCのコードを可能にするが、デバッグをさらに困難なものにする。

専門家の中には未定義の処理を引き起こさない言語を指して、メモリセーフ言語（あるいは単にセーフ言語）という用語を使う者もいる。そのような言語では配列の領域外にアクセスするようなことはない。

弱い型付けとは、言語が型の暗黙的な変換（またはキャスト）をするという意味である。再び例を挙げる。

var x := 5;
var y := "37";
x + y;

弱い型付けの言語でこのようなコードを書くと、どのような（型の）結果が得られるのか自明ではない。Visual Basicなど、実行すると42という結果を出す言語もあり、そのような処理系は演算が意味のあるものになるように文字列"37"を数値の37に変換する。またJavaScriptなど、"537"という結果を出す言語もあり、そのような処理系は数値5を文字列"5"に変換し、文字列同士を連結する。どちらの言語でも、結果の型を決定する規則では両方のオペランド（演算子の左と右の値）が考慮されている。AppleScriptなどの言語では、結果の型は左のオペランドの型のみによって決定される。

+演算子を文字列連結など加算以外の用途に使わないなど、演算子オーバーロードの使用を減らすことで、このような混乱を減らすことができる。例えば、.（ピリオド）や&（アンパサンド）を文字列連結に使う言語もある。

注意深い言語設計によって、C#やJavaなどが持つ型検査やそれによる保護を失わずに、言語を利便性のために弱い型付けであるように見せかける（型推論などのテクニックを用いて）こともできる。

[編集] 型の安全性

プログラミング言語の型システムを分類する3つめの方式は、型付けされた処理や型変換の安全性によるものである。計算機科学ではある言語が誤った状態を引き起こす処理や変換を許さないとき、その言語は「型安全」(type-safe) であるという。

例を再掲する。

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

前述したように、Visual Basic などの言語では変数 z の値は42となる。この動作がプログラマの意図したものであってもそうでなくとも、言語はこの結果を明確に定義しており、プログラムがクラッシュしたり、z に不定な値が代入されてしまうようなことはない。このような動作をする言語は型安全である。

C で同じ例を考えてみる。

int x = 5;
char y[] = "37";
char* z = x + y;

この例では z はyのアドレスに5加えた先のメモリの内容を参照する。言い換えれば y が指す文字列の終端のヌル文字の2バイト先を指している。その位置のデータは不定（プログラムで定義されていない）であり、おそらくアドレス可能なメモリの外側にあるので、ここで z をデリファレンスするとプログラムの終了を引き起こすことがある。これは型付けされているが、メモリセーフではないプログラムの例である。型安全な言語ではこのような状況は起こりえない。

[編集] ポリモーフィズムと型

詳細は「ポリモーフィズム」を参照

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

[編集] ダック・タイピング

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

[編集] 論争

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

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

[編集] 脚注

[編集] 参考資料

• Advanced Topics in Types and Programming Languages by Benjamin C. Pierce
• Type System Terminology
• Meijer, Erik and Peter Drayton. "Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages". Microsoft Corporation. 2007-03-08 閲覧。

[編集] 関連項目

• データ型
• 多重定義
• 再帰データ型