計算機科学において、型安全性（type safety）とは、プログラミング言語が型エラーをどの程度抑制または防止するかを示す性質である。型安全な言語は、強い型付け（strongly typed）または厳密な型付け（strictly typed）の言語と呼ばれることもある。あるプログラミング言語において型エラーに分類される振る舞いは、通常、適切でないデータ型の値に対して操作を行おうとすることで生じる。例えば、文字列と整数を加算しようとする場合などがこれに当たる。
型規則の適用は、潜在的なエラーをコンパイル時に検出する静的なもの、値に型情報を関連付け、実行時に必要に応じてその情報を参照することで、発生しようとしているエラーを検出する動的なもの、あるいはその両方を組み合わせたものがある。静的な方式で不正とみなされるプログラムでも、動的な方式なら実行できる場合が多い。ただし、その代わりにエラーが実行時に発生する可能性がある。
静的（コンパイル時）型システムの文脈では、型安全性には通常、ある式が最終的にとる値が、その式の静的型に属する正当な値であることの保証などが含まれる。ただし、厳密な要件はこれほど単純ではない。例えば、サブタイピングやポリモーフィズムによって事情は複雑になる。
定義 イギリスの計算機科学者ロビン・ミルナーは、次のように述べている。
適切に型付けされたプログラムは「間違った動作をしない」。
型システムが健全であるなら、その型システムによって受理された式は、別の無関係な型の値を生成したり、型エラーによって異常終了したりするのではなく、適切な型の値に評価されなければならない。AT&Tの研究者Vijay Saraswatは、これに関連して次のように定義している。
ある言語において、データに対して実行できる操作が、そのデータの型によって許可されたものに限られるなら、その言語は型安全である。
プログラムが「適切に型付けされている」ことや「間違った動作をする」ことが何を意味するかは、各プログラミング言語に固有の静的意味論および動的意味論によって定まる。したがって、型健全性の厳密かつ形式的な定義は、言語の仕様記述に用いられる形式意味論の流儀によって異なる。計算機科学者のAndrew K. WrightとMatthias Felleisenは、操作的意味論によって定義された言語について、型安全性を定義し証明するための手法を定式化した。この手法では、言語が型健全であるとみなされるためには、その意味論が次の2つの性質を満たさなければならない。
進行（Progress） 適切に型付けされたプログラムは決して行き詰まらない。すべての式は、すでに値であるか、明確に定められた方法によって値に向けてさらに簡約できる。 保存（Preservation、または型保存（subject reduction）） 各評価ステップの後も、それぞれの式の型は変化しない。すなわち、その型は「保存」される。
型健全性については、表示的意味論や構造的操作意味論に基づく、他の形式的な定式化も数多く発表されている。
他の安全性との関係 型健全性は、それ自体では、型システムの規則が内部的に整合していることを示すにすぎない。しかし、プログラミング言語は、適切に型付けされていることによって、次のような他の性質も保証されるよう設計される場合がある。
不正な操作の防止。例えば、除算演算子は文字列を除数とする演算として定義されていないため、型システムは式 3 / "Hello, World" を不正なものとして拒否できる。 メモリ安全性 型システムは、ある型のオブジェクトへのポインタを別の型のオブジェクトへのポインタとして扱うことによって生じうる、不正なポインタを防止できる。 依存型をサポートするような、より高度な型システムでは、範囲外へのアクセスを検出して拒否することで、潜在的なバッファオーバーフローを防止できる。 異なる型の<a href="./意味論_(言語学)" rel="mw:WikiLink">意味</a>に起因する<b><a href="./論理の誤り" rel="mw:WikiLink">論理エラー</a></b>。例えば、インチとミリメートルはいずれも整数として格納できるが、両者を互いに置き換えたり、そのまま加算したりすべきではない。型システムでは、これらに異なる整数型を割り当てることで、そのような操作を防止できる。
型安全な言語と型安全でない言語 型安全性は、学術的なプログラミング言語研究で提案される実験用の小規模な言語（toy language）や難解プログラミング言語では、通常、満たすべき要件の一つとされる。しかし、多くの言語は、人手で型安全性を証明するには規模が大きすぎる。これは、その証明に数千もの場合分けの検証が必要になることが多いためである。一方、厳密に定義された意味論を持つStandard MLのように、型安全性のある定義を満たすことが証明されている言語もある。 Haskellのような他の言語についても、特定のエスケープ機能を使用しない限り、何らかの型安全性の定義を満たすと考えられている。例えば、Haskellの unsafePerformIO は、通常は入出力（I/O）が行われる制限された環境から抜け出すために使用される機能であり、型システムを迂回するため、型安全性を破る目的にも使用できる。型のパンニングも、このようなエスケープ機能の一例である。言語の定義上どのような性質が保証されているかにかかわらず、実装上のバグや、他の言語で記述されたリンク先のライブラリのバグによって、実行時にエラーが発生する場合がある。このようなエラーによって、特定の状況では、その言語のある実装が型安全でなくなることがある。Sunによる初期のJava仮想マシンには、この種の問題に対する脆弱性が存在した。
強い型付けと弱い型付け プログラミング言語は、型安全性の特定の側面を表すために、口語的に強い型付けまたは弱い型付け（あるいは緩い型付け）に分類されることがある。1974年、LiskovとZillesは、強い型付けの言語を「オブジェクトが呼び出し側の関数から呼び出される関数へ渡される際、その型が、呼び出される関数で宣言された型と互換性を持たなければならない」言語と定義した。 1977年、Jacksonは「強い型付けの言語では、それぞれのデータ領域が固有の型を持ち、それぞれのプロセスは、それらの型を用いて通信に必要な条件を指定する」と述べた。 これに対して、弱い型付けの言語では、予測不能な結果が生じたり、暗黙の型変換が行われたりすることがある。
メモリ管理と型安全性 型安全性は、メモリ安全性と密接に関係している。例えば、ある型 が特定のビットパターンのみを有効な値として許容する言語の実装を考える。ダングリングポインタによるメモリエラーがあると、すでに無効となった型 の変数に、 の正当な値を表さないビットパターンを書き込めてしまい、その変数を読み出した際に型エラーが発生する可能性がある。逆に、ある言語がメモリ安全であるなら、任意の整数をポインタとして使用することは許されない。そのため、ポインタまたは参照には、整数とは別の型が存在しなければならない。
最低限の条件として、型安全な言語では、異なる型の割り当て領域をまたいでダングリングポインタが有効になることを許してはならない。しかし、多くの言語では、メモリ安全性や重大な障害の防止のために厳密には必要でない場合であっても、プログラマが定義した抽象データ型が正しく使用されるように制約を課している。各割り当て領域には、その内容を表す型が与えられ、その型はその領域が存在する間は固定される。これにより、型に基づくエイリアス解析では、異なる型を持つ割り当て領域は互いに異なるものであると推論できる。
型安全な言語の多くはガベージコレクションを使用している。Pierceは、ダングリングポインタの問題があるため、「明示的な解放操作が存在する場合に型安全性を実現することは極めて困難である」と述べている。 一方、Rustは一般に型安全な言語とみなされており、ガベージコレクションの代わりに借用検査器を用いてメモリ安全性を実現している。
オブジェクト指向言語における型安全性 オブジェクト指向言語では、通常、型システムが存在すること自体に型安全性が組み込まれている。これはクラス定義によって表現される。
クラスは、そのクラスから生成されるオブジェクトの構造と、それらのオブジェクトを扱うための契約としてのAPIを本質的に定義する。新たに作成される各オブジェクトは、その契約に従う。
特定のクラスから生成されたオブジェクト、または特定のインターフェースを実装するオブジェクトを受け渡す各関数も、その契約に従う。したがって、その関数内でオブジェクトに対して許される操作は、そのオブジェクトが実装するクラスのメソッドによって定義されたものに限られる。これにより、オブジェクトの整合性が保たれることが保証される。Type safety is hence also a matter of good class definition: public methods that modify the internal state of an object shall preserve the object itegrity
ただし、オブジェクトの構造を動的に変更できるオブジェクト指向言語や、リフレクションを用いてオブジェクトの内容を変更し、クラスのメソッド定義によって課される制約を回避できる言語は例外である。
特定の言語における型安全性の問題
Ada Adaは、組み込みシステム、デバイスドライバ、その他のシステムプログラミングに適するよう設計される一方で、型安全なプログラミングを促すことも意図されている。これらの相反する目標を両立させるため、Adaでは型安全でない操作を、通常 Unchecked_ で始まる名前を持つ特定の特殊な構文に限定している。Unchecked_Deallocation は、あるAdaのプログラム単位に pragma Pure を適用することで、その単位内で事実上使用を禁止できる。プログラマには、Unchecked_ 構文を十分慎重に、必要な場合にのみ使用することが求められる。これらを使用しないプログラムは型安全である。
SPARKはAdaのサブセットであり、Adaに存在しうる曖昧さや安全性上の問題を排除するとともに、静的に検査される契約を言語機能として追加している。SPARKでは実行時のメモリ割り当てを全面的に禁止することで、ダングリングポインタに関する問題を回避している。
Ada 2012では、事前条件、事後条件、および型不変条件という形で、静的に検査される契約が言語自体に追加された。
C C言語は、限定的な状況では型安全である。例えば、ある構造体型へのポインタを別の構造体型へのポインタに変換しようとすると、明示的なキャストを使用しない限り、コンパイル時エラーが発生する。しかし、非常によく使われる操作の中にも型安全でないものが数多く存在する。例えば、整数を出力する一般的な方法として printf("%d", 12) のような記述がある。この場合、%d は printf に対して、実行時に整数の引数が渡されることを期待するよう指定している。一方、printf("%s", 12) のように、文字列へのポインタを期待するよう関数に指定しながら整数の引数を渡すコードも、コンパイラによっては受理される場合があるが、その結果は未定義となる。この問題は、gccなど一部のコンパイラが、printf の引数と書式文字列との型の対応関係を検査することで、ある程度軽減されている。
さらにC言語はAdaと同様に、動作が未規定または未定義となる明示的な型変換を提供している。またAdaとは異なり、C言語ではこうした型変換を利用する慣用的な記述が非常に一般的であり、このことがC言語に型安全でないという評価を与える一因となっている。例えば、ヒープ上にメモリを確保する標準的な方法は、必要なバイト数を引数として malloc などのメモリ確保関数を呼び出すことである。この関数はvoidポインタ（void*）を返し、呼び出し側のコードではこれを適切なポインタ型へ明示的または暗黙的に変換する必要がある。標準化以前のC言語の実装では、この変換に明示的なキャストが必要であった。そのため、ある struct Foo の領域を確保する場合には、Foo* foo = (struct Foo*)malloc(sizeof(struct Foo)) のようなコードが一般的な書き方となった。 現在のC言語では、malloc() が返す void* を明示的にキャストする必要はない。一方、C++では型安全性のため、この変換には明示的なキャストが必要となる。
C++ C++は一般に、その前身であるC言語よりも型安全である。例えば、void* から他のポインタ型への暗黙の型変換を許可しないほか、次のような機能を備えている。
new 演算子は、malloc が void* を返すのに対し、指定された型に対応するポインタを返す。 C++では、仮想関数やテンプレートを使用することで、void* を用いずに型安全なポリモーフィズムを実現できる。 dynamic_cast など、より安全なキャスト演算子が用意されている。dynamic_cast はポインタや参照に対して実行時の型検査を行う。一方、static_cast は変換元と変換先の型についてコンパイル時に検査を行い、一般にC言語形式のキャストより安全である。 C++11で導入された強い型付けの列挙型（enum class とも呼ばれる）は、整数や他の列挙型との間で暗黙に型変換されない。 C++の explicit コンストラクタ、およびC++11で導入された explicit 変換演算子は、暗黙の型変換を防止する。
C# C#は型安全な言語である。型付けされていないポインタもサポートしているが、これを使用するには unsafe キーワードが必要であり、コンパイラの設定によって使用を禁止できる。また、実行時のキャスト検証を標準でサポートしている。as キーワードを使用したキャストでは、変換が無効な場合に null 参照が返される。一方、C言語形式のキャストでは、変換が無効な場合に例外が送出される。詳しくはC#の変換演算子を参照。
他のすべての型の基底となる object 型に過度に依存すると、C#の型システムの利点を損なうおそれがある。一般には、object への参照を使用するよりも、C++のテンプレートやJavaのジェネリクスに相当するジェネリクスを使用する方が望ましい。
Java Javaは、型安全性を保証するよう設計されている。Javaにおける処理はすべてオブジェクトの内部で行われ、各オブジェクトはクラスのインスタンスである。
型安全性を実現するため、各オブジェクトは使用される前にメモリが割り当てられている必要がある。Javaではプリミティブ型も使用できるが、適切に割り当てられたオブジェクトの内部でのみ使用できる。
型安全性の一部が間接的に実現される場合もある。例えば、BigDecimal クラスは任意精度の浮動小数点数を表すが、有限桁で表現できる数のみを扱う。BigDecimal.divide() は、2つの BigDecimal として表された数の除算結果を新しいオブジェクトとして生成する。
この場合、例えば 1/3 = 0.33333… のように除算結果を有限桁で表現できないとき、演算に丸めモードが指定されていなければ、divide() メソッドは例外を送出することがある。したがって、オブジェクトがクラス定義に暗黙に含まれる契約を満たすことは、言語そのものではなくライブラリによって保証される。
Standard ML Standard MLは厳密に定義された意味論を持ち、型安全であることが知られている。しかし、Standard ML of New Jersey（SML/NJ）、その構文上の派生であるMythryl、およびMLtonなど、一部の実装では型安全でない操作を提供するライブラリが用意されている。これらの機能は、特定のメモリ配置を必要とすることのあるCライブラリなどの非MLコードと連携するため、それぞれの実装が備える外部関数インターフェースと併用されることが多い。もう一つの例として、SML/NJの対話的トップレベル自体が挙げられる。これは、利用者が入力したMLコードを実行するために、型安全でない操作を使用する必要がある。
Modula-2 Modula-2は強い型付けの言語であり、安全でない機能には明示的にそのことを示すことを要求する、という設計思想を持つ。これは、そのような機能を SYSTEM と呼ばれる組み込みの擬似ライブラリへ「移動」し、使用する前にそこからインポートしなければならないようにすることで実現されている。これにより、安全でない機能が使用されていることがインポート文から明示的に分かるようになる。しかし、この方針は当初の言語仕様書およびその実装では一貫して適用されていなかった。 型キャストの構文や、Pascalから継承されたバリアントレコードなど、事前にインポートすることなく使用できる安全でない機能が依然として残っていた。 これらの機能を SYSTEM 擬似モジュールへ移すことが困難だったのは、それらの機能を表すインポート可能な識別子が存在しなかったためである。インポートできるのは識別子のみであり、構文そのものをインポートすることはできない。IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *) VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS; addr := SYSTEM.ADR(word);
(* but type cast syntax can be used without such import *) VAR i : INTEGER; n : CARDINAL; n := CARDINAL(i); (* or *) i := INTEGER(n);ISO Modula-2規格では、型キャストについてこの問題が修正され、型キャスト構文は CAST という関数に変更された。この関数を使用するには、SYSTEM 擬似モジュールからインポートする必要がある。しかし、バリアントレコードなど、その他の安全でない機能については、SYSTEM 擬似モジュールから何もインポートせずに引き続き使用できた。IMPORT SYSTEM; VAR i : INTEGER; n : CARDINAL; i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)最近の言語改訂では、当初の設計思想がより厳密に適用された。まず、そこからインポートされる機能が安全でないことをより明確にするため、擬似モジュール SYSTEM は UNSAFE に改名された。次に、残っていた安全でない機能はすべて、完全に削除されるか（例えばバリアントレコード）、UNSAFE 擬似モジュールへ移された。インポート可能な識別子が存在しない機能については、その機能を有効化するための識別子が新たに導入された。このような機能を有効にするには、対応する有効化用識別子を UNSAFE 擬似モジュールからインポートしなければならない。その結果、現在では UNSAFE からのインポートを必要としない安全でない機能は、言語内に残されていない。IMPORT UNSAFE; VAR i : INTEGER; n : CARDINAL; i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)
FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *) <*FFI="C"*> (* pragma for foreign function interface to C *)
Pascal Pascalには、型安全性に関するいくつかの要件があり、その一部は一部のコンパイラでも維持されている。Pascalコンパイラが「厳密な型付け」を要求する場合、2つの変数の間で代入を行うには、両者の型が互換であるか（例えば整数から実数への変換）、または同一の部分型でなければならない。例えば、次のようなコード断片があるとする。type TwoTypes = record I: Integer; Q: Real; end;
DualTypes = record I: Integer; Q: Real; end;
var T1, T2: TwoTypes; D1, D2: DualTypes;厳密な型付けの下では、TwoTypes として定義された変数は DualTypes と互換ではない。これは、両者を構成する要素が同一であっても、ユーザー定義型そのものが同一ではないためである。したがって、T1 := D2; という代入は不正となる。一方、T1 := T2; という代入は、両者が同一の部分型として定義されているため有効である。ただし、T1.Q := D1.Q; のような代入は有効である。
Common Lisp 一般に、Common Lispは型安全な言語である。Common Lispのコンパイラは、型安全性を静的に証明できない操作について、動的な検査を挿入する役割を担う。ただし、プログラマは、動的な型検査の水準を下げてプログラムをコンパイルするよう指定できる。 このようなモードでコンパイルされたプログラムは、型安全であるとはみなせない。
C++ の例 以下の例は、C++のキャスト演算子を誤って使用すると、型安全性が損なわれる可能性があることを示している。最初の例では、基本データ型が不正にキャストされる場合を示す。#include <iostream> using namespace std;
int main () { int ival = 5; // integer value float fval = reinterpret_cast<float&>(ival); // reinterpret bit pattern cout << fval << endl; // output integer as float return 0; }この例では、reinterpret_cast によって、整数から浮動小数点数への安全な変換が行われないようコンパイラに明示的に指示している。 プログラムを実行すると、意味のない浮動小数点値が出力される。この問題は、代わりに float fval = ival; と記述することで回避できる。
次の例では、オブジェクトへの参照が不正にダウンキャストされる場合を示す。#include <iostream> using namespace std;
class Parent { public: virtual ~Parent() {} // virtual destructor for RTTI
class Child1 : public Parent { public: int a;
class Child2 : public Parent { public: float b;
int main () { Child1 c1; c1.a = 5; Parent & p = c1; // upcast always safe Child2 & c2 = static_cast<Child2&>(p); // invalid downcast cout << c2.b << endl; // will output garbage data return 0; }2つの派生クラスは、それぞれ異なる型のメンバを持っている。基底クラスへのポインタを派生クラスへのポインタにダウンキャストした場合、得られたポインタが正しい型の有効なオブジェクトを指しているとは限らない。この例では、その結果として意味のない値が出力される。この問題は、static_cast を、無効なキャストを検出できる dynamic_cast に置き換えることで回避できる。
関連項目
型理論
注釈
出典