型システム

型システム（かたシステム、英: type system）は、コンピュータプログラミングの数々の構成要素および値に対して、型（type）と呼ばれる特性を付与するための数々の規則群から成立している形式体系である。型の付与は、型付け（typing）と言われる。例えば、変数・式・関数・モジュール・オブジェクトなどが型の付与対象になり、それらの型付け要素を規則的な関係でまとめたデータ構造にも型は付与されてカテゴライズされる。

型システムの目的は、プログラムエラーとバグの発生を抑止することである。そのための型安全性とは、各計算および各オペレーションでの型エラー（不正計算、ロジックエラー、バッファオーバーフロー、不正ポインタなど）の発生を防止することと同義になる。

型システムは、一般的に型理論をベースにしている。

定義と性質

型の例

型とは

→「データ型」も参照

プログラミング言語はさまざまな値を扱う。代表的かつ最も原始的なものは数値や文字列だが、一般的に有限の資源制約があるコンピュータにとって都合のよい内部表現が使われ、例えば数値には32ビットや64ビットといった固定サイズの整数型や浮動小数点数型が、文字列には特定の文字コード集合によって符号化された整数値の羅列（文字配列）が使われることが多い。文字列の表現には最後の文字（番兵）に0を使用するゼロ終端文字列（ヌル終端文字列）が使われることもあれば、長さ情報を別途整数値で保持する複合データ構造が使われることもある。三角関数は浮動小数点数を引数にとり浮動小数点数を返す。先頭の文字を大文字にする関数は文字列を引数にとり文字列を返す。ユーザーからの入力を数値として扱うためには、文字列を解釈して数値を返す関数が必要である。ここで、3.14 や "hoge" といった値について「浮動小数点数」や「文字列」といった種類に分類して扱っているが、同じ種類の値であれば同じ操作（演算）が可能である。この「値の種類」が型（データ型）である。

型検査

プログラムにおけるエラーはさまざまだが、型に基づく一連のエラーがある。単純な例としては、浮動小数点数を表現しているワードを（一般的なコンピュータのハードウェアでは、メモリ上のワードとしては区別がつかないため）整数型として扱ってしまう、といったようなものである。この例では 0 と +0.0 のような特別な場合を除いてたいていの場合は得られる結果は無意味であり、より複雑な構造を持った値の場合は構造を壊して不正にしてしまうかもしれない。このような異常をプログラムが起こさないことを検査するのが型検査（英: type checking）である。

型の安全性

型にまつわるものに限らず、プログラムの安全性（safety）とは、プログラミング言語や文脈によって定義が異なる場合があり、一概に述べることはできない。ひとつの指標として、プログラムが言語仕様で定義されていない「未定義」の状態に陥らない、という性質のことを指すことがある。たとえばC言語やC++の標準では、NULLポインタのデリファレンスや、配列の範囲外アクセスによるバッファオーバーランなど、そういった「未定義」の動作を引き起こすケースが決められている。大抵の実行環境では、NULLポインタのデリファレンスによってセグメンテーション違反（アクセス違反）が引き起こされ、オペレーティングシステムによってプログラムが異常終了させられることになるが、必ずしもそうなるとは限らず、実際には何が起こるか分からない。「安全な」プログラムを記述するためには、言語未定義の動作を避けるように注意深くコーディングしなければならない。この指標の観点では、プログラムのエラーを、言語未定義や処理系依存の異常動作によってではなく、ランタイムやインタプリタが検出して仕様通りに異常終了するような場合は「安全」の側に含まれることになる。一般的に仮想マシン上で動作するJavaやC#のような言語は、ランタイムによって検証され、信頼されたコードのみを実行する仕組みが用意されているため、C/C++よりも安全である。未定義動作はコンピュータセキュリティと密接な関係があり、例えばバッファオーバーランが引き起こされると悪意のある不正なコードを実行できてしまったりするセキュリティホールにつながることがある。ただし安全なチェック機構のある言語ほどオーバーヘッドが大きくなるため、安全性は実行速度とのトレードオフの関係にある。

例えば、JavaではNullオブジェクトを参照した場合、実行時にNullPointerException例外がスローされると言語仕様で規定されており、この点でC言語やC++よりも安全であると言える。しかし、JavaではNullオブジェクトを参照するコードを記述しても言語構文上は合法とみなされるため、コンパイラによるチェック機構は働かず、実行時にNullPointerExceptionがスローされるまでプログラミングミスに気づかない可能性がある。さらに進んだKotlinのように「Null安全」な言語では、Nullの状態を許容しない型を定義することができ、このNull非許容型を使う限りはNullオブジェクトを参照することはないことが保証される。また、Kotlinでは主にJavaとの相互運用のためにNullの状態を許容する型も定義できるが、このNull許容型を使う場合は、事前にNullチェックコードを記述することを言語仕様によって強制されるため、安全性が増す。

そして型にまつわる安全性のことを型安全性（英: type safety）と呼ぶが、一般的に型安全性とは、データ（オブジェクト）の本来の型に従ってプログラムを正しく実行できる性質のことを指す。前述のように型安全性が具体的にどのようなものであるかはプログラミング言語や文脈に依存する。

一般的にコンピュータでは整数と浮動小数点数のように異なる型の値同士の演算はできず、いったん同じ型に揃えて演算する必要がある。プログラマがコード上で型変換（キャスト）を明示する必要のある厳しい言語もあれば、コンパイラによってある程度の暗黙の型変換や型昇格がなされるようなゆるい言語もある。さらにCにおいては、キャスト（型変換）構文を使うと、互換性のない型同士でも強制変換できてしまう。例えば整数とポインタとの間で相互変換することや、整数へのポインタを浮動小数点数へのポインタに無理やり変換することもできてしまい、簡単に型安全性が破壊される。誤った型へのポインタ経由で領域にアクセスした場合の動作は未定義である。型検査によって型安全性を確保するために、互換性のない型同士の変換は明示的・暗黙的問わず一切できないようになっている言語や、間違った型変換をすると実行時に例外をスローする言語もある。

型安全でない例としては、C/C++において、可変長引数の関数を利用する場面が挙げられる。代表的なものがprintfやscanfで、これらの関数は任意の数のあらゆる型のデータ（オブジェクト）を可変長引数として統一的に渡せるように、いったん引数オブジェクトの型情報を消去し、別途入力として与えられた書式文字列をもとに型情報を関数内部で復元する仕組みになっている。しかし書式文字列の指定にミスがあると、本来のオブジェクトの型とは異なる誤った型として取り出すことになってしまうが、型が消去されてしまっているためにコンパイラはミスを検出することができない。結果として、想定されたものとは異なるでたらめな値が出力されてしまったり、間違った型へのポインタを経由することで誤った領域にデータを書き込んでしまいクラッシュしたり、といった未定義の異常動作を引き起こす。一方、JavaやC#の可変長引数では、実引数として渡される個々のオブジェクト自身が型情報を保持しており、書式指定ミスによる型の不一致があった場合は例外をスローして安全にプログラムを中断・異常終了させることができるため、C/C++よりも型安全性が高い。

別の例として、ジェネリックプログラミング（ジェネリクス）をサポートしていなかった初期のJavaやC#では、可変長の動的配列や双方向リストなどのコレクションに型Tのオブジェクトを格納する場合はいったん基底型であるjava.lang.ObjectやSystem.Objectにアップキャストし、またコレクションからオブジェクトを取り出す場合は型Tにダウンキャストしなければならず、正しい型のオブジェクトとして取り出すためには注意深くコーディングする必要があった。ジェネリクスをサポートすることで、コレクションに格納する型Tを静的に決めることができるようになり、誤ったキャストにより実行時エラーを引き起こす可能性を排除できるようになった。このような改善も型安全性の向上とみなされる。

型の互換性

静的型付き言語の型検査では、すべての式の型がその式が現れた文脈で期待される型と一貫しているか、検証しなければならない。たとえば、x := eという代入文では式eの推論される型は変数xの宣言型または推論型と一貫していなければならない。この一貫性の概念を互換性といい、プログラミング言語ごとに固有のものである。

明らかなように、eとxの型が同一でかつその型への代入操作が許可されているなら、これは正当な式である。したがって最も単純な型システムでは、2つの型が互換であるかどうかは2つの型が同一である（または等価である）かどうか（等価性）という単純な問題に置き換えることができる。別の言語では2つの式が同じ型を持つと理解されるのに別の基準を採用している。これら、型の「同一性理論」は非常に多岐にわたっており、2つの対極の例は構造的型システムと名前的型システムとである。構造的型システムとは外部に見せている構造（インタフェース、特に暗黙的なもの）が同じものを持つ値を同じ型であるとするもので、名前的型システムとは型宣言の構文からのみ型の同一性を判定する（型が同じ「名前」を持たなければならない）ものである。

オブジェクト指向言語のように基底型と派生型の関係がある言語では、互換性の関係はより複雑なものとなる。型Derivedが型Baseの派生型であるとすると、Derived型の値はBase型の値が必要とされる文脈で使用することができる（リスコフの置換原則）。しかし逆は真ではない。等価性と同様に派生型の関係はプログラミング言語によって異なった方法で定義され、多くのバリエーションが存在しうる。パラメータ付けされたまたはアドホックなポリモーフィズムを持つ言語の存在は型の互換性に何らかの意味を持つのかもしれない。

型付けの分類

静的な型付けと動的な型付け

→詳細は「静的型付け」および「動的型付け」を参照

静的（static）と動的（dynamic）は、プログラム要素の型を検査（check）する際の性質である。これは検査タイミングを示している。

プログラムの実行前（コンパイル時、インタプリタ開始時）に型検査を行うのが静的型付けであり、プログラムを実行しながら型検査を行うのが動的型付けである。Javaは一般に静的型付け（静的型付き言語）であるが、ダウンキャストは明示する必要があり実行時に型検査を受ける。Common Lispは一般に動的型付け（動的型付き言語）だが、type specifierという静的に型を指定する文法も持っている。このように、ある程度は混在している言語もある。さらに、静的検査が行われるタイミングについても、コンパイル時の他リンク時やインタプリタのソースコード読み込み時といった場合もありえるため、簡単に見た目では分類できないこともある。

型なし

型付けを更に厳密に定義した区分として型なし（英: untyped）という区分が存在する。代表的な言語としてはSmalltalk、BCPL、B言語、アセンブリ言語などがある。Smalltalkでは高速化のため処理系依存で実行時に型検査することがあるものの言語的には型検査がなく、動的型付け言語のように文字列に割り算をするといった不正な操作をしても処理系が型検査して停止する事は無い。

BCPL、B言語、アセンブリ言語などオブジェクト指向とは関係なく型を持たない言語では、ハードウェアのワード長に依存した1種類の型のみを持つか、言語を使う側でデータを参照するときにデータ幅や種類の解釈を決定することとなる。

オブジェクト指向型の型なしの言語では処理系が型検査をしない代わり、ライブラリで例外を投げて停止する。例えばSmalltalkではオブジェクトに対し対応するメソッドが存在しないメッセージを投げると、最終的にクラスごとに定義した#doesNotUnderstand:メソッドに至る。このメソッドが例外を投げるようになっていれば停止するが、そうでなければ停止することなく走り続ける。対照的に動的型付け言語では、演算子のような一部の操作について値の型に応じた型検査を処理系が行いエラーとしてしまう。エラー発生時の挙動については言語によって異なり、例えば数値を文字列値で割るという2 / 'A'のような無意味な演算に対して、PythonはTypeError例外をスローし、JavaScriptはNaNを返す。型なしのオブジェクト指向言語は最適化がしづらい反面、オブジェクトの操作を処理系に制限されないため使用者が後から自由にオブジェクトの操作を追加できる利点がある。

強い型付けと弱い型付け

強い（strong）と弱い（weak）は、静的/動的型付けでのプログラム要素の型を解釈（interpret）する際の性質である。

強い型付けとは、プログラミング言語仕様内でデータ値の型を解釈するという全く普通の方法に従ったものである。暗黙的型変換（implicit type conversion）と型強制（type coercion）と型ジャグリング（type juggling）は、言語仕様内なので、こちら側になる。基底型を派生型にするなど一定の型制約での実行時型チェック付きの型キャスト（type casting）も、こちら側になる。特殊な例では、LISP風の潜在的型付けやダックタイピングによる型解釈も言語仕様内なので、こちら側である。

弱い型付けとは、言語仕様外になる明示的型変換（explicit type conversion）と型キャスト（type casting）の使用によって、データ値の型を様々に解釈できる変則的な方法を大幅に許容したものである。型安全性は保証されなくなる。具体例としては以下がある：

数値用例

明示的型変換によって、実数型を整数型に丸める。整数型を実数型に拡張する。ワード値をバイト値に切り詰める。バイト値をワード値に拡張して拡張部分を0で埋めるなど。

ポインタ用例

主にvoidポインタを型キャストして、あらゆる型を表わす。

タグ無し共用体用例

タグ無し共用体を明示的型変換して、あらゆる型を表わす。

型パンニング（type punning）用例

明示的型変換によって、ビット列と数値型を変換する。アドレス値と数値型を変換する。文字型/文字列と数値型を変換する。レコードのバイト列を切り詰めたり拡張したりして基底レコードと派生レコードを変換するなど。

明示的な型付けと暗黙的な型付け

→詳細は「型推論」を参照

明示的（explicit）と暗黙的（implicit）は、静的型付けでのプログラム要素の型を宣言（declare）する際の性質である。

明示的な型付けとは、プログラマがその型を指名して変数を定義（宣言）するスタイルである。これはFORTRANやC言語などの手続き型プログラミングに適したものであり、大抵のプログラミング言語はこちらを採用している。

暗黙的な型付けとは、型を指名しないで変数を定義（宣言）するスタイルである。その変数の型は、等号式で結び付けられたリテラル、他の変数、リテラルと他の変数を引数にした関数、関数の組み合わせなどを再帰的に辿って解釈することで、コンパイラによって自動的に導き出される。これは型推論と呼ばれる。型推論は、関数型プログラミングの参照透過性に準拠したatom（初期リテラル）とvalue（評価値）によるデータ値表現に適したものであり、MLやHaskellなどで採用されている。従来の手続き型やオブジェクト指向プログラミング言語においても、型推論の機能を導入するケースが増えている。

コード中の数値や文字列のリテラルおよび式は型を暗示する。例えば、式 3.14 はおそらく浮動小数点数を暗示し、式 1, 2, 3 はおそらく整数のリスト（主に配列）を暗示する。リテラルがどのような型になるかは言語によって異なる。ユーザー定義のリテラルを記述することができる言語もある。リテラル自体がオブジェクトであり、変数に束縛することなくメソッドやプロパティを使用できる言語もある。

名前的型付けと構造的型付け

→「en:Nominal type system」および「en:Structural type system」も参照

名前的（nominal）と構造的（structural）は、静的/動的型付けでのプログラム要素の型を識別（identify）する際の性質である。

名前的型付けとは、システムが保持しているプログラム要素の参照情報上の型の名前を見て、データ値の型を識別するスタイルである。

構造的型付けとは、参照情報上の型の名前を見ないで、データ値本体の分析でデータ値の型を識別するスタイルである。ただし、データ集合を分解して行き着くリテラルの型識別は事実上の名前的型付けになる。例えば構造体では、フィールド構造（各フィールドの型の種類と順序）が一致しているならばフィールド名が違っても同じ型と判定される。構造的型付けは、部分型の判定にも多用される。例えばオブジェクトでは、特定の関数/手続きの構造を双方が所持しているならば、その部分型での等価と見なされる。特定のフィールド構造を双方が所持している場合も同様である。

ダックタイピング

ダックタイピングは、構造的型付けに類似した型付けのスタイルであり、オブジェクトが対象になることが多い。例えばオブジェクトが特定のプロパティ/フィールド/変数を所持しているか、または特定のメソッド/関数/手続きを所持しているならば等価判定される。これも部分型（サブタイプ）視点である。この等価判定は、エラー発生のないプロパティ参照またはメソッド実行に直結している。ダックタイピングの名称は、帰納法の一種であるダックテストに由来している。

『もしアヒル (a duck) のように歩いて、アヒルのように鳴くなら、それはおそらくアヒルだ』

さらに動的型付けに基づく動的ダックタイピングと、静的型付けに基づく静的ダックタイピングがある。特にC++のテンプレートは静的ダックタイピング機能の典型であり、例えば関数呼び出し演算子をオーバーロードした関数オブジェクトを定義することで、関数ポインタと区別することなく統一的にアルゴリズムの述語オブジェクトとして扱うこともできる。適切な演算子オーバーロードを定義することで、組み込みの数値型やポインタ型と同じ記法で扱える型をユーザー定義することもできる。

分類には諸説あり、「ダックタイピングは実行時の動的な型付けであり、構造的型付けはコンパイル時の静的な型付けである」とみなす者もいれば、「構造的型付けはコンパイル時の静的なダックタイピングである」とみなす者もいる。

型推論

→詳細は「型推論」を参照

静的な型システムの言語では型宣言を必要とし、基本的にプログラマはすべての変数に特定の型を明示的に関連付けなければならない。しかし、変数の初期化時の右辺値や変数の使われ方など、プログラマが型を明示せずともコードの文脈から型を自動的に決定する型推論（type inference）の機能を持つ言語もある。例として、Haskellにおいて変数 x と y を加算する関数 f を定義してみる。

f x y = x + y

ここで、x と y の型を特に明示していないが、+による加算は数値のみに定義されているので、コンパイラは x と y は共に数値型であると推論できる。ゆえにプログラム中で f の引数として数値でない型（文字列やリストなど）の値を渡して呼び出すとエラーを報告する。

main = do
  print (f 1 2) -- 3
  print (f 1.0 2.0) -- 3.0
  --print (f "hoge" "fuga") -- コンパイルエラー。

型推論の目的は、単にコードの記述効率を向上したり、型のミスマッチに起因するエラーを軽減したりすることだけではない。ラムダ式や匿名型など、コンパイラが内部で型を自動生成し、プログラマが具体的な型の名前をコード上で書き下すことができない場合もあり、そういった機能に対応しなければならないという目的もあって型推論を導入した言語もある（C++やC#など）。

議論

型付けについて

静的型付き言語はいわゆるコンパイラ言語に、動的型付き言語はいわゆる動的プログラミング言語によくみられる。

型検査がどのように働くのかを見るために、次の擬似コードを考える。

var x;
x := 5;
x := "hi";

この例では、1行目でxという名の変数を宣言し、2行目でxに整数5を代入し、3行目でxに文字列"hi"を代入している。ほとんどの静的型付けの処理系ではこのようなコードは不正（型エラー）となる。なぜなら2行目と3行目でxに一貫性のない型の値を代入しているからである。

対照的に動的型付けの処理系では、型は変数ではなく値に付けられるので、上のようなコードが実行できる。動的型付けの処理系は間違った文や式を実行したときに、値の誤用に関するエラーを型エラーとして捕捉する。つまり、動的型付けはエラーをプログラムの実行中に捕捉する。動的型付けの典型的な実装ではプログラム中のすべての値が型情報を持ち、演算に値を使う前に型情報を確かめる。例を挙げる。

var x := 5;
var y := "hi";
var z := x + y;

このコードでは、1行目でxを値5で束縛し、2行目でyを値"hi"で束縛し、3行目でxとyを足そうとしている。動的型付き言語ではxを束縛した値は(整数, 5)というペアとして表すことができ、yを束縛した値は(文字列, "hi")というペアで表すことができる。プログラムが3行目を実行しようとしたとき、処理系は整数と文字列という型情報を検査し、もし演算+（加算）がその2つの型について定義されていなかったら、エラーを出す。

プログラミング言語の中には、静的に型検査されないコードをプログラマが書けてしまう「バックドア」を持つものもある。例として、JavaやC風の言語には「キャスト」がある。

プログラミング言語が静的型付けをもつことは必ずしも動的型付けをもたないことを意味するわけではない。例えばJavaは静的型付けを採用しているが、処理によっては動的な型情報の取得を必要とするものもあり、それらは動的型付けの一形態とみなせる。静的型付けと動的型付けの違いについては様々な議論がある。

静的および強い型付けの支持者と動的および自由な型付けの支持者の間では衝突が度々おきる。前者のグループは厳密な型付けの使用によって、処理系がより多くのエラーを問題が大きくなる前に発見できるようになると主張している。後者のグループはより気軽な型付けによってコードはよりシンプルなものになり、そのようなコードは解析しやすいとされるので、エラーは減少すると主張している。型推論がある言語では型を手で宣言する必要はほとんどないので、強い型付けに伴う開発のオーバーヘッドは低減される。

個人がどのグループに分かれるかは、開発しているソフトウェアの種類やチームのメンバーの能力、他のシステムとの対話性の度合い、開発チームの規模などに依ることが多い。少人数で小回りのきくプロジェクトには気軽な型付けがより合い、フォーマルで大人数で仕事が分断されている（プログラマ、アナリスト、テスト部隊、など）プロジェクトは厳密な型付けのほうがうまくいくことが多い、と結論づける者もいる。

TypeScriptのように、JavaScriptの持つ動的型付けにまつわる問題点を回避して大規模アプリケーション開発にも耐えうるようにするため、静的型付けをサポートするよう改良された言語もある。

型の利点について

最適化

静的な型検査によってコンパイラは最適化に有用な情報を得ることがある。例えばデータ構造アライメントの指定によって、ある型の値が16の倍数のアドレスに配置されることが保証されていれば、コンパイラはより効率の良いマシン命令を選択できる。

可読性の向上

より表現力の高い型システムでは、型はプログラマの意図を説明することができるので、型自身がドキュメントの役割を果たし、可読性の向上に寄与することもある。例として、何らかの時刻情報（タイムスタンプ）を返す関数を定義するとき、単なる64ビットの組み込み整数型ではなく専用のタイムスタンプ型（構造体型など）を返す関数として宣言すると、その型情報が関数の意味を記述していることになる。

抽象性/モジュール性の確立

型によってプログラマは低レベルでの実装に煩わされずにより高レベルで考えることができるようになる。これはプログラム設計に適切な抽象化をもたらす。例えば文字列型によってプログラマは文字列を文字列として、単なるバイトの列ではないものとして考えることができる。

また型によって複数のデータ構造の間の依存関係を明確にすることができ、さらに上位レベルでは複数のサブシステム間のインタフェースを表現することができる。これはサブシステムの相互運用性に必要な定義を局所化し、それらのサブシステムが通信する際に起きる矛盾を防止するなど、モジュール性の向上に貢献する。

型のトレードオフについて

静的型付けか動的型付けかの選択はいくつかのトレードオフを必要とする。

静的型付けは型エラーをコンパイル時にある程度確実に発見する。よって最終的なプログラムの信頼性を上げるはずである。しかしながら、型エラーがどれほど犯しやすい間違いなのか、その内の何割が静的型付けで検出できるのか、という点についてプログラマの意見は割れている。静的型付けの支持者は型検査されたプログラムの方が信頼性が高いと信じており、それに対して動的型付けの支持者は実際に流通しているソフトウェアの信頼性では大差ない点を指摘している。

静的型付けは大抵、より高速に実行可能なコンパイル済みコードを生成する。コンパイラが正確なデータ型を知っていれば、最適化されたコードを生成できる。さらに、静的型付き言語のコンパイラではショートカットをみつけるのもより簡単になる。この理由からCommon Lispなどのいくつかの動的型付き言語では随意で型宣言ができるようになっている。最適化のための型付けは静的型付けの影響で普及した。

対照的に、動的型付けのほうがコンパイラやインタプリタの動作が高速になることがある。動的型付けの言語ではソースコードが変更されてもやり直すべき解析が少ないためである。これは「編集-コンパイル-テスト-デバッグ」というサイクルの時間を減らす。

型推論のない静的型付き言語ではプログラマがメソッドや関数の型を宣言しなければならない。これはプログラムの追加的なドキュメントとして機能することがあり、コンパイラによってコードと同期させることが強制される。しかし型宣言のない静的型付き言語もあるので、これは静的型付けのというよりは型宣言の報酬である。言語が型推論の機能を持っていたとしても、型推論による暗黙的型付けを多用しすぎると可読性やメンテナンス性がかえって低下することがある。型推論を使用することが適切ではないケースについて一定のガイドラインが示されていることもある。

動的型付けはいくつかの静的型付けでは不正となり実現できない仕組みを可能にする。例えばデータをコードとして実行するeval関数である。さらに動的型付けでは、具体的なデータ構造の代わりに文字列を暫定的に用いることなどがやりやすく、プロトタイピングとの相性も良い。

動的型付き言語のメタプログラミング機能はより強力で使いやすいことが多い。例を挙げると、C++のテンプレートはRubyやPythonでの等価なコードより、書くのが煩わしい。またイントロスペクションのような、より高度な実行時の仕組みを静的型付き言語で使うのは、さらに困難になることが多い。

型のバリエーション

典型的には、プログラム中ではすべての値には1つの特定の型が付けられる（1つの型が複数の派生型を持つ場合でも）。オブジェクトやモジュール、通信路、依存関係、及び型自身にさえ型が付けられることもある。

また、型システムの理念であるコンパイル時に重点を置いたフォールトアヴォイダンスを更に推し進めている拡張的な形式体系にエフェクトシステムというものがある。こちらではプログラム副作用をも体系化して一種の型として扱っている。

型とポリモーフィズム

→詳細は「ポリモーフィズム」を参照

ポリモーフィズム（多相）という語は、コード（具体的には関数やクラス）が複数の型の値に基づいて動作できること、または同じデータ構造の異なるインスタンスが異なった型の要素を持てることを指す。型システムによってはコードの再利用性を改善するためにポリモーフィズムを持つものもある。ポリモーフィズムのある言語ではプログラマはリストや連想配列のようなデータ構造を使用される要素の型ごとにではなく、単に一度だけ実装すればよい。この理由から計算機科学ではこの種のポリモーフィズムの利用はジェネリックプログラミングと呼ばれることがある。ポリモーフィズムの型理論における基礎は抽象化やモジュール、また（場合によっては）派生型についての研究と密接な関連がある。

参考資料

• Benjamin C. Pierce (2005). Advanced Topics in Types and Programming Languages. MIT Press. ISBN 0-262-16228-8. http://www.cis.upenn.edu/~bcpierce/attapl/main.html 
• Type System Terminology
• Meijer, Erik. “Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages” (PDF). Microsoft Corporation. 2007年2月16日時点のオリジナルよりアーカイブ。2007年3月8日閲覧。
• Pierce, Benjamin C. 著、遠藤侑介・ほか共 訳『型システム入門 : プログラミング言語と型の理論』オーム社、2013年3月。ISBN 9784274069116。 

関連項目

• 型理論 - 型システムの土台。
  • カインド (型理論)
  • System F
  • ラムダキューブ
  • 依存型
• ポリモーフィズム
  • 多重定義（アドホック多相）
  • 総称型（パラメトリック多相）
  • 派生型（サブタイプ多相）
  • 抽象型
  • インタフェース (抽象型)