型システムの意義(TAPL第1章より)

『アンダースタンディング コンピュテーション』に続いて、『型システム入門―プログラミング言語と型の理論』を読む。

型システムの定義

システムが仕様通りに動作するかどうかを保証する形式手法と呼ばれるものにはいろいろあるけど、利用が難しい。もっと簡単に使えるような軽量形式手法として普及しており、確立されてもいるのが型システムである。

型システムとは、プログラムの書く部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的な手法である。

(本書 p.1より)

型システム(型理論)には、論理学・数学におけるいろんな理論からの流れもあるけど、本書では、上記の定義にある通り、プログラムの動作に関する推論のためのツールという側面にフォーカスしてみていく。また、型システムを、プログラミングにおける項を値の性質によって分類し、実行中にそれらの項がどう振る舞うかの静的な近似を求めるためのものとみなす。

型システムの効用

型システムで何ができるかについて、以下6つを挙げる。

1. エラーの検出
2. 抽象化
3. ドキュメント化
4. 言語の安全性
5. 効率性
6. その他

エラーの検出

ある種のエラーを早期に検出できること。具体的には、異なる型どうしで計算しようとしてしまう不注意のようなものから、科学計算で単位を勘違いする概念上の誤りのようなことまで。ここで「ある種の」といっているのは、たとえば、ゼロ除算であるとか、配列へのアクセスが範囲内に収まっているかといった実行時のエラーなどのような、実行時エラーを除く、ということ。

ただ、このメリットを享受するには、プログラマが適切にデータ構造を型付けして表現しなければならない。たとえば、複雑なデータ構造をなんでもリストで表現してしまっては、せっかくの型システムが活かされなくなってしまう。

抽象化

大規模なシステムをモジュール化するに際して、型がモジュール(クラスなども含む)間のインタフェイスを曖昧さなく定義するのに役立つ。また、型がもたらすそのような抽象性により、実装と切り離して設計や議論を行うことができる。

ドキュメント化

設計者にとってのみならず、プログラムを読む側にも型は有用である。コメントと違い、コードに埋め込まれ、コンパイルするたびに検査されるため、実装とドキュメントとに齟齬をきたすこともない。

言語の安全性

言語の「安全性」とは何か？

平たく言えば、安全な言語とはプログラミングの最中にうっかり自分の足を撃つことが不可能な言語であると定義できる。

この直感的な定義を少し洗練すれば、安全な言語とは自らがもたらす抽象を保護するものであるといえるだろう。

具体的には、Cのように、メモリの抽象としての配列を提供しつつも、配列の範囲外へのアクセスが可能であるような言語は「安全」ではないということ。

ただし、静的型安全性がすなわち言語の安全性というわけではない。動的型検査を行う言語であっても、実行時に安全でない操作をチェックすることで、ここでいう安全性を達成することができる。

効率性

コンパイラは、型情報により適切な機械語命令を用いることができ、また、前述の動的検査を除去することができる等、最適化を行える。

その他

プログラミングだけでなく、ネットワークのセキュリティ、プログラムの解析ツール、自動定理証明、DTDやXMLスキーマといった分野に、あれこれと応用されている(よくわからない)。

型システム入門 −プログラミング言語と型の理論−