型システム

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

型システムの概要

プログラム中の項が実行時にどう振る舞うかの静的な近似を求めるものとみなせる

プログラムがある種の振る舞いを起こさないことは断定的に証明できるが、起こすことは証明できない

保守的である

型検査器はコンパイラやリンカの中に組み込まれるので、計算量的に扱いやすい解析でないといけない

型システムでできること

エラーの検出

プログラムをリファクタリングしたとき、依存する部分を手作業で探すのではなく、型検査が失敗した部分を直せば済む

インターフェースは、モジュールやクラスの型だとみなすことができる

インターフェースを抽象的に考えることで、良い設計に繋がり、そのモジュールの提供者と利用者の意思疎通ができる

ドキュメント化

コード品質の向上、レビューコストの削減

人間のためのインターフェース

プログラムに書かれた型を読むことで、振る舞いを理解する有用なヒントになる

コメントと違って、コンパイルが実行されるたびに検査されるので古くなることがない

開発者の意図がわかり、間違った使い方をさせない

go to definitionなど

言語の安全性

「安全」であると、プログラムの実行中に未定義の状態にならない

メモリなどのハードが提供する抽象を、安全な言語では抽象的に扱うことができる

安全でない言語では、プログラムがどう動作するのかをメモリ内のデータ構造のレイアウトやコンパイラが配置する順序と行った低水準な詳細をプログラムが全て意識しなければならない

安全でない静的型付け言語はC,C++など

本来なら静的検査で全て検査されるべきだが、例えばリストのインデックスアクセスが要素数を超えていたことに対するエラーは静的な型検査では捕捉できず、実行時の境界検査に頼る

効率性

コンパイル時に型検査器が収集する情報に依存して、最適化などをしている

関数の取りうるものの場合の数が減る

その他

セキュリティ

自動定理証明

データベース

型は仕様

型付けの種類

型の表現力

型の表現力が乏しいと

エラーの誤検知頻発

検出できるエラーの範囲が狭い

プログラムが冗長になる

型の表現力が豊富すぎると、

プログラムに型が与えられるかの判定が複雑になる

型の強弱

強い型付け

高度な型システム

テストと型検査

テスト

'有限個の入力'でプログラムが使用を満たすかどうかを'実行'して確認

型検査

'任意の入力'について、プログラムが仕様を満たすかどうかを'実行せず'に確認

いろんな型システム

参考資料

この記事にいろいろ良さそうなリンクがある