以前書いた（C言語についての） メモリ安全性について定義した記事 について、型安全性について説明する記事も投稿してほしいというコメントがありました。型安全性についてはかなりよく知られてきていると思いますが、ズバリこうだと簡単に定義できるほどにはまだ理解が浸透していません。特に誰かが”Javaは型安全な言語だ”と言った場合、これは厳密に何を意味するのでしょう。全ての型安全な言語はある意味”同じ”と言えるでしょうか。ある特定の言語について、そして一般的な意味で、あなたを悩ませる型安全性とは何でしょうか。

実際のところ、型安全性が何を意味するのかは言語の型システムの定義によります。最もシンプルなケースでは、型安全性はプログラムの動作が正しく定義されるように保証します。もっと一般的な話をすると（この記事ではそのあたりをカバーするつもりですが）、言語の型システムはそのプログラムの正確さと安全性を推論するための強力なツールとして使えます。ですから、新しい型システムの開発は大きな研究分野なのです。

基本的な型安全性

型安全性と聞いてパッと思い浮かぶイメージを、次のフレーズは簡潔に要約しています。” 正しく型付けされたプログラムは不正な動作をしない “。このフレーズは Robin Milner が1978年に出した論文、 プログラミングにおける型ポリモーフィズムについての考察 に書かれています。このフレーズを分解して部分ごとに定義してみましょう。まず後半からです。

不正な動作

プログラム言語を定義するものはシンタックス（プログラムを記述するための規則）と、 セマンティクス （プログラムの意味）の2つです。全ての言語が直面する問題なのですが、多くのプログラムで、シンタックス上は正しくてもセマンティクス上は問題があるということがあります。よく知られる言語学の例として、Chomskyの”Colorless green ideals sleep furiously（無色の緑色の考えが猛烈に眠る）”という文があります。シンタックス上は完全に正しいけれど、意味をなしていません。OCamlプログラム言語での例を挙げると、 1+”foo” があります。この言語のセマンティクスによれば、このようなプログラムは意味がありません。他にも、C言語の { char buf[4]; buf[4] =’x’ } がありますね。インデックス4への書き出しは宣言されたバッファの領域外にあり、言語仕様はこのアクションを未定義、すなわち無意味だとみなします。このような無意味なプログラムが実行されれば、 不正な動作 と言えるでしょう。

正しく型付けされている→不正な動作をしない

言語の型システムは、型安全な言語において”正しい”（間違っていない）プログラムだけが通過できるように保証する特別な方法です。具体的には、型システムが条件を満たしたプログラムだと判断すれば、そのプログラム（またはプログラムフェーズ）は正しく型付けされていると言えます。型安全は正しく型付けされたプログラムが決して不正な動作をしないように保証します。そういうプログラムは（正しく定義された）意味を持つことになります。下図はその状況を視覚化しています。

型安全な言語においては、正しく型付けされたプログラムは、正しく定義されたプログラムのサブセットであり、それらは更に全ての（シンタックス的に正しい）プログラムのサブセットとなります。

どの言語が型安全なのか

さて、それでは よく知られている言語 が型安全かどうか考えてみましょう。言語が違えば、型安全性の意味も変わってくるのでしょうか。

C言語とC++：型安全ではない。 C言語の標準的な型システムは、一般的（および常識的）に無意味と見なされるプログラム、つまりバッファの領域外に書き込むようなプログラムを除外しません。 ^(1) ですからC言語についていえば、正しく型付けされたプログラムでも不正な動作をする可能性があります。C++は（事実上）C言語の上位集合なので、C言語の型安全性の欠如を受け継いでしまっています。

Java、C#：（恐らく）型安全。 成熟した言語の実装が型安全かどうかについて見極めるのはとても難しいのですが（例えば ジェネリクスの初期バージョンはバグが多かった ）、より小型に形式化され、おそらくはJavaと本質的に同等である言語（例えば Featherweight Java ）は型安全です。 ^(2) 興味深いのは、C言語のセマンティクスが未定義だとみなす動作について、これらの言語は意味を持たせているという点です。この事実によって、型安全かどうかが決まっているのです。中でも注目すべきなのは、C言語では境界を越えた配列にアクセスするプログラムは意味を持たないのに、JavaとC#では意味を持ちます。例えばJavaは例外処理として ArrayBoundsException を実行します。

Python、Ruby：（ほぼ間違いなく）型安全。 PythonやRubyは動的型付き言語とよく言われますが、実行時のシグナルの型エラーに対して例外処理を実行します。Javaが ArrayBoundsException を実行するように、Rubyは整数型と文字列型を連結しようとすると例外処理を実行するのです。どちらの場合もプログラムの動作は言語のセマンティクスに基づいていることから、このプログラムは正しく定義されていると言えます。実際、言語のセマンティクスはすべてのプログラムに意味を与えるものなので、先ほどの図の 正しく定義されたプログラム の輪と、すべてのプログラムの輪は一致します。このように、これらの言語はnull許容型システム ^(3) なので型安全であると考えられます。あらゆるプログラムを許容し、決して不正な動作を引き起こすことはありません（3つの輪がすべて重なり合うことになります）。ゆえに型安全なのです。

この結論に疑問を感じる方がいるかもしれません。Javaでは o.m() という記述が正しく型付けされていると見なされれば、型安全性によって、 o は引数のないメソッド m を持つオブジェクトであることが保証されます。ですから関数の呼び出しは常に成功します。Rubyでは、同様の記述 o.m() は（null許容）型システムによって、常に正しく型付けされていると見なされます。しかし実行時に o がメソッド m を定義する保証はありません。ですから、関数の呼び出しは成功するのか例外エラーに終わるのかは分かりません。

つまり、型安全性が意味するところは１つではないということです。何を保証するのかは、言語のセマンティクスによります。言語のセマンティクスは不正な動作とは何であるかを暗黙に定義するからです。Javaでは存在しないメソッドの呼び出しは不正となりますが、Rubyではそうではありません。存在しないメソッドを呼び出すと例外エラー ^(4) を返すだけです。

基本の先へ

一般的な型安全性は有用なものです。型安全がなければ、実行するプログラムが適切に定義されているという保証は得られません。保証がないと、本質的にどんな動作も可能になってしまいます。未定義の動作を許容してしまうというCやC++の性質は、 スタックスマッシング や フォーマットストリング攻撃 など様々なセキュリティ上の弱点の原因となります。型安全な語にはこのような弱点はありません。

一方で、これまでRubyとJavaについて見てきたように、全ての型システムが同じように作られているわけではありません。プロパティを保証するものもあれば保証できないものもあります。このように、言語が型安全かどうかを単純には問えません。問うべきなのは、型安全によって何ができるのかということです。最後に、型システムによって何ができるのか、現在進めている研究によって得た豊富な実例からいくつかご紹介しましょう。

ギャップを埋める

前出の 正しく型付けされたプログラムの輪と正しく定義されたプログラム の輪は、ぴったりと重なってはいません。この2つ輪のギャップとなるのが、正しく定義されてはいても型システムが拒絶してしまうプログラムです。以下に例を挙げます。ほとんどの型システムはこのプログラムを拒絶します。

if (p) x = 5;
  else x = "hello";
if (p) return x+5;
  else return strlen(x);

上記のプログラムは常に整数を返しますが、型システムは拒絶するかもしれません。というのも、変数xが整数かつ文字列として扱われているからです。静的解析で例えるならば、 以前Heartbleedに関する記事で述べたように 、型システムは 健全 であっても 完全とは言えない ということです。不完全な型システムはプログラマに余計な負担を強います（それが プログラマがPythonやRubyなどの動的言語を使いたくなる理由の1つかもしれません ）。解決策を１つあげるとすれば、このギャップを埋め、より多くのプログラムを許容できるような型システムを設計することです。

そうした設計を実際に行う場合の例として、Javaの型システムがバージョン1.5で ジェネリクス の概念を取り入れて機能拡張したことが挙げられます。Javaバージョン1.4では、プログラムを許容する型システムを保証するためにはキャストが必要でした。しかしバージョン1.5では、キャストは不要です。更に例を挙げると、関数型プログラミング言語の基礎である ラムダ計算 があります。 Milnerのポリモーフィック型システム は 2階（またはより高階の）ポリモーフィズム をサポートする型システムよりもプログラムの許容性が低いのですが、それよりも許容性が低いのが、ラムダ計算の 単純型の型システム です。（より完全性が高く）表現力があり、 なおかつ 有用な型システムの設計は研究しがいのある分野なのです。

不変条件の強制

一般的なプログラミング言語には int 型 と string 型 があります。型安全性で int 型 の実質的な内容をプログラムで確実に表現するようにしています。そして実行時に、-1、2、47などの値を評価します。しかし話は int 型だけにとどまりません。型システムは実に様々な型への対応が可能で、プログラムを記述する際には多種多様なプロパティを表現することができます。

例えば、最近、論理式を使って型が取り得る値のセットを詳細化する詳細型の研究コミュニティに多くの関心が集まってきています。 {v: int | 0 <= v} 型は、 0 <= v ,という式で int 型 を詳細化し、事実上、自然数の型を定義します。詳細型のおかげでプログラマはデータ構造の型の中にデータ構造の不変条件を記述することができ、型安全性により、不変条件は常に保持されることを保証されています。詳細型システムは、他の言語の中でも特にHaskellやF#（それぞれ LiquidHaskell 、 F7 と呼ばれる）のために開発されました。

別の例を挙げましょう。不変条件を強制すれば、型システムを使って データ競合 を避けられます。ここで言う不変条件とは、共有変数に対して、その値を保護するためにロックを行っているスレッドだけがアクセスできるようにするものです。共有変数の型にはその変数を保護するロックが記述されます。 安全なロックのための型 がAbadiとFlanaganによって初めて提唱されて、C言語（ Locksmith ）や Javaへ実装すべく 開発されてきました。

汚染されたデータの使用を制限したり 、 個人情報の公開を防いだり 、（オブジェクトが解放された後に使用されないように） 型状態 と呼ばれる厳密なプロトコルに従ってオブジェクトを使用したり するように設計された型システムなど、他にもたくさん例があります。

型抽象と情報隠蔽

多くのプログラミング言語は、プログラマが データ抽象 （ 情報隠蔽 とも）を確実に行えるようにすることを目指しています。これらの言語では、クラスやモジュールや関数のように、抽象化して記述することができ、それらを使用するクライアントコードからは内部が分からないように隠しておくことができます。そうすることで、クライアントコードに影響を与えずに内部を変更することができるため、より堅牢で保守しやすいプログラムになります。

型システムは抽象を強制する上で重要な役割を果たすことができます。例えば、うまく設計された型システムを用いて、プログラムは抽象化に依存するだけで、実装方法には依存しないという 表現独立 を証明できます。また、型が強制された抽象は、Wadlerが見事に示したように、 自由定理 を実現してくれるものになり得ます。故 John Reynolds は、型と抽象に関して画期的な研究を行い、1983年に発表した 型、抽象、そしてパラメータポリモーフィズム という論文の中で型と抽象について特に詳しく述べています。この論文には「 型構造は抽象のレベルを維持するためのシンタックスの規律です 」という有名な一節があります。つまり、保守しやすいシステムの構築において型が 基本的な 役割を担っていると断定しています。

最後に

型安全性は重要なプロパティです。少なくとも、型安全な言語は、その言語のプログラムが正しく定義されていることを保証します。この保証は、プログラムの動作を推論するのに必要で、セキュリティを考慮しなければならない時には特に重要です。しかし、型システムはもっと様々なことができます。プログラムについて推論するための基礎を作ることができ、不変条件の強制や抽象化の維持を確実に行うこともできます。ソフトウェアはこれまで以上に普及してより複雑になってきているので、型システムは、私たちが頼りにしているシステムを安全で信頼できるようにするために重要なツールです。

型システムについてもっと学びたいなら、『 Types and Programming Languages 』 邦訳 や『 Advanced Topics in Types and Programming Languages 』といった Benjamin Pierce の本から始めることをお勧めします。

この記事の草稿を見て意見や提案をしてくれた Matthew Hammer や Jeff Foster 、 David Van Horn に感謝します。

注釈：