この記事には複数の問題があります。改善
やノートページでの議論にご協力ください。型システム
主要カテゴリ
静的型付け vs 動的型付け
強い vs 弱い
明示的 vs 型推論
名前的 vs 構造的
ダックタイピング
マイナーカテゴリ
部分型
再帰型
部分構造型
依存型
漸進的型付け
フロータイピング
潜在的型付け
型理論のコンセプト
直積型 - 直和型
交差型 - 共用型
単一型 - 選択型
帰納型 - 精製型
トップ型 - ボトム型
函数型 - 商型
全称型 - 存在型
一意型 - 線形型
型システム（かたシステム、英: type system）は、コンピュータプログラミングの数々の構成要素および値に対して、型（type）と呼ばれる特性を付与するための数々の規則群から成立している形式体系である[1]。型の付与は、型付け（typing）と言われる。例えば、変数・式・関数・モジュール・オブジェクトなどが型の付与対象になり、それらの型付け要素を規則的な関係でまとめたデータ構造にも型は付与されてカテゴライズされる。
型システムの目的は、プログラムエラーとバグの発生を抑止することである[2]。そのための型安全性とは、各計算および各オペレーションでの型エラー（不正計算、ロジックエラー、バッファオーバーフロー、不正ポインタなど）の発生を防止することと同義になる。
型システムは、一般的に型理論をベースにしている[3]。
定義と性質型の例
型とは「データ型」も参照
プログラミング言語はさまざまな値を扱う。代表的かつ最も原始的なものは数値や文字列だが、一般的に有限の資源制約があるコンピュータにとって都合のよい内部表現が使われ、例えば数値には32ビットや64ビットといった固定サイズの整数型や浮動小数点数型が、文字列には特定の文字コード集合によって符号化された整数値の羅列（文字配列）が使われることが多い。文字列の表現には最後の文字（番兵）に0を使用するゼロ終端文字列（ヌル終端文字列）が使われることもあれば、長さ情報を別途整数値で保持する複合データ構造が使われることもある。三角関数は浮動小数点数を引数にとり浮動小数点数を返す。先頭の文字を大文字にする関数は文字列を引数にとり文字列を返す。ユーザーからの入力を数値として扱うためには、文字列を解釈して数値を返す関数が必要である。ここで、3.14 や "hoge" といった値について「浮動小数点数」や「文字列」といった種類に分類して扱っているが、同じ種類の値であれば同じ操作（演算）が可能である。この「値の種類」が型（データ型）である。 プログラムにおけるエラーはさまざまだが、型に基づく一連のエラーがある。単純な例としては、浮動小数点数を表現しているワードを（一般的なコンピュータのハードウェアでは、メモリ上のワードとしては区別がつかないため）整数型として扱ってしまう、といったようなものである。この例では 0 と +0.0 のような特別な場合を除いてたいていの場合は得られる結果は無意味であり、より複雑な構造を持った値の場合は構造を壊して不正にしてしまうかもしれない。このような異常をプログラムが起こさないことを検査するのが型検査（英: type checking）である。 型にまつわるものに限らず、プログラムの安全性（safety）とは、プログラミング言語や文脈によって定義が異なる場合があり、一概に述べることはできない。ひとつの指標として、プログラムが言語仕様で定義されていない「未定義」の状態に陥らない、という性質のことを指すことがある。たとえばC言語やC++の標準では、NULLポインタのデリファレンスや、配列の範囲外アクセスによるバッファオーバーランなど、そういった「未定義」の動作を引き起こすケースが決められている。大抵の実行環境では、NULLポインタのデリファレンスによってセグメンテーション違反（アクセス違反）が引き起こされ、オペレーティングシステムによってプログラムが異常終了させられることになるが、必ずしもそうなるとは限らず、実際には何が起こるか分からない。「安全な」プログラムを記述するためには、言語未定義の動作を避けるように注意深くコーディングしなければならない。この指標の観点では、プログラムのエラーを、言語未定義や処理系依存の異常動作によってではなく、ランタイムやインタプリタが検出して仕様通りに異常終了するような場合は「安全」の側に含まれることになる。一般的に仮想マシン上で動作するJavaやC#のような言語は、ランタイムによって検証され、信頼されたコードのみを実行する仕組みが用意されているため、C/C++よりも安全である。未定義動作はコンピュータセキュリティと密接な関係があり、例えばバッファオーバーランが引き起こされると悪意のある不正なコードを実行できてしまったりするセキュリティホールにつながることがある[4]。ただし安全なチェック機構のある言語ほどオーバーヘッドが大きくなるため、安全性は実行速度とのトレードオフの関係にある。 例えば、JavaではNullオブジェクトを参照した場合、実行時にNullPointerException例外がスローされると言語仕様で規定されており、この点でC言語やC++よりも安全であると言える。しかし、JavaではNullオブジェクトを参照するコードを記述しても言語構文上は合法とみなされるため、コンパイラによるチェック機構は働かず、実行時にNullPointerExceptionがスローされるまでプログラミングミスに気づかない可能性がある。さらに進んだKotlinのように「Null安全」な言語では、Nullの状態を許容しない型を定義することができ、このNull非許容型を使う限りはNullオブジェクトを参照することはないことが保証される。
型検査
型の安全性
