型システム（type system）とは、プログラミング言語において値や式をデータ型に分類し、型を扱い、またそれらが相互作用する方式を定義する仕様及び実装である。 1つの型は共通の汎用的意味または用途を持つ値の集合1つを表現する。[1]型システムは言語ごとに非常に異なっているが、おそらく最も大きな違いはその文法および実行時における動作においてである。
コンパイラでは値の記憶効率や値に対する操作アルゴリズムの選定を最適化するために静的型が用いられることがある。例として多くのCコンパイラではfloat型を単精度浮動小数点数のためのIEEE標準にしたがって32ビットで表現する。よって加算、乗算等に各浮動小数点数演算が用いられる。
型の強制の度合いや評価方法は言語の型付け（typing）に影響する。さらに、ポリモーフィズムのある言語では一つの演算がいくつかの具象アルゴリズムに対応付けられる。型理論は型システムを対象とした形式的な研究であるが、実際のプログラミング言語の型システムはコンピュータ・アーキテクチャや言語設計及び処理系の実装の実用上の課題から生まれたものである。
目次
1 基礎
2 型検査
2.1 静的な型付けと動的な型付け
2.1.1 トレードオフ
2.2 強い型付けと弱い型付け
2.3 型の安全性
3 ポリモーフィズムと型
3.1 ダック・タイピング
4 明示的または暗黙的な型の宣言と型推論
5 互換性（等価性と派生型）
6 論争
7 脚注
8 参考資料
9 関連項目
//
型を割り当てること（「型付け」）によってビットの集まりに意味が与えられる。型は通例、メモリ中の値と変数の両方と関連する。コンピュータではすべての値は単なるビットの集まりなので、ハードウェアはメモリアドレスやオペコード、キャラクタ、整数、浮動小数点数などの基本的なデータの間でさえ何の区別も行わない。型はプログラムとプログラマにそれらのビット列をどのように扱うべきかの情報を与える。
型システムがもたらす主要な機能には以下のようなものがある。
安全性
型の使用によってコンパイラが無意味な、または不正であろうコードを検出することが可能になる。例えば人間は "Hello, World" / 3 という式を見ると、文字列を整数で（通常の感覚では）割ることができないので、不正であると認識できる。強い型付けはさらなる安全性をもたらすが、必ずしも完全な安全性を保証するものではない。
最適化
静的な型検査によってコンパイラは最適化に有用な情報を得ることがある。例えばある型の値が4の倍数のアドレスに配置されることが保証されていれば、コンパイラはより効率の良いマシン命令を使うことができるかもしれない。
可読性
より表現力の高い型システムでは型はプログラマの意図を説明することができるので、ドキュメントの役割を果たすこともある。例としてタイムスタンプが整数の派生型である環境において、プログラマが単なる整数ではなくタイムスタンプを返す関数を宣言すると、その型情報が関数の意味を記述していることになる。
抽象化またはモジュール化
型によってプログラマは低レベルでの実装に煩わされずにより高レベルで考えることができるようになる。例えば文字列型によってプログラマは文字列を文字列として、単なるバイトの列ではないものとして考えることができる。また型によってプログラマは2つのサブシステム間のインタフェースを表現することができる。これはサブシステムの相互運用性に必要な定義を局所化し、それらのサブシステムが通信する際に起きる矛盾を防止する。
典型的には、プログラム中ではすべての値には1つの特定の型が付けられる（1つの型が複数の派生型を持つ場合でも）。オブジェクトやモジュール、通信路、依存関係、及び型自身にさえ型が付けられることもある。例を挙げると
データ型
値の型
クラス
オブジェクトの型
カインド
型の型
などがある。
プログラミング言語ごとにある型システムは型付けされたプログラムがどのようにふるまい得るかを規定し、その規則から外れたふるまいを不正であると判定する。