タイプシステム

型エラーは、演算が期待していた型とは異なる型のデータを受け取ったときに発生します。^{[ 4 ]}例えば、コード行が2つの整数を割り算しているときに、整数の代わりに文字列が渡された場合、型エラーが発生します。^{[ 4 ]}これは意図しない状態であり^{[注2 ]、}プログラム開発の複数の段階で発生する可能性があります。したがって、型システムにはエラーを検出する機能が必要です。Haskellなどの一部の言語では、型推論が自動化されているため、コンパイラにリントが用意され、エラーの検出に役立てることができます。

型安全性はプログラムの正しさに貢献しますが、型チェック自体が決定不能問題（停止問題など）になるという代償を伴ってのみ正しさを保証できる場合があります。自動型チェックを備えた型システムでは、プログラムが正しく実行されないことが判明しても、コンパイラエラーが発生しないことがあります。ゼロ除算は安全でない誤った操作ですが、コンパイル時にのみ実行される型チェッカーは、ほとんどの言語でゼロ除算をスキャンしません。ゼロ除算は実行時エラーとして顕在化します。これらの欠陥がないことを証明するために、プログラム解析と呼ばれる他の種類の形式手法が一般的に使用されています。あるいは、依存型言語のように十分に表現力のある型システムであれば、これらの種類のエラーを防ぐことができます（例えば、ゼロ以外の数値の型を表現するなど）。さらに、ソフトウェアテストは、そのような型チェッカーでは検出できないエラーを見つけるための経験的な方法です。

静的型チェックとは、プログラムのテキスト（ソースコード）を分析することで、プログラムの型安全性を検証するプロセスです。プログラムが静的型チェッカーに合格すれば、そのプログラムはあらゆる入力に対して、一定の型安全性を満たすことが保証されます。

静的型チェックは、プログラム検証の限定的な形態（型安全性を参照）とみなすことができ、型安全な言語においては最適化の一種とも考えられます。コンパイラがプログラムの型が適切であることを証明できれば、動的安全性チェックを出力する必要がなくなり、結果としてコンパイルされたバイナリの実行速度が向上し、サイズも小さくなります。

チューリング完全な言語の静的型チェックは、本質的に保守的です。つまり、型システムが健全（つまり、すべての不正なプログラムを拒否する）かつ決定可能（つまり、プログラムが正しい型であるかどうかを判断するアルゴリズムを作成できる）である場合、その型システムは不完全でなければなりません（つまり、実行時エラーが発生しないにもかかわらず、拒否される正しいプログラムが存在する）。^{[ 7 ]}例えば、次のコードを含むプログラムを考えてみましょう。

if <complex test> then <do something> else <signal that there is a type error>

実行時に式が<complex test>常に と評価される場合でもtrue、静的アナライザーでは分岐がelse実行されないことを判断するのが難しい（不可能ではないにしても）ため、ほとんどの型チェッカーはプログラムを型が不正であるとして拒否します。^{[ 8 ]}その結果、静的型チェッカーは、めったに使用されないコード パスの型エラーを迅速に検出します。静的型チェックがない場合、 100% のカバレッジを持つコード カバレッジテストでも、このような型エラーを見つけることができない可能性があります。テストでは、値が作成されるすべての場所と、特定の値が使用されるすべての場所の組み合わせを考慮する必要があるため、このような型エラーを検出できない可能性があります。

ダウンキャストなど、多くの有用で一般的なプログラミング言語機能は、静的にチェックすることができません。そのため、多くの言語では静的型チェックと動的型チェックの両方が採用されています。静的型チェッカーは検証可能な部分を検証し、動的型チェックは残りの部分を検証します。

静的型チェックを備えた多くの言語では、型チェッカーを回避する方法が用意されています。一部の言語では、プログラマーが静的型安全性と動的型安全性のどちらかを選択できます。たとえば、C# では従来、変数は静的に宣言されていましたが、[9]:77、セクション 3.2、C# 4.0 では^{、実行時に動的に}チェックdynamicされる変数を宣言するために使用されるキーワードが導入されました。 ^{[ 9 ] : 117、セクション 4.1}他の言語では、型安全でないコードを記述できます。たとえば、Cでは、プログラマーは同じサイズの任意の 2 つの型の間で値を自由にキャストできるため、型の概念を事実上覆すことができます。

動的型チェックとは、実行時にプログラムの型安全性を検証するプロセスです。動的型チェック言語の実装では、一般的に各実行時オブジェクトに、その型情報を含む型タグ（つまり、型への参照）を関連付けます。この実行時型情報（RTTI）は、動的ディスパッチ、遅延バインディング、ダウンキャスト、リフレクションプログラミングなどの機能の実装にも使用できます。

ほとんどの型安全な言語には、静的型チェッカーも備えている場合でも、何らかの形の動的型チェックが含まれています。^{[ 10 ]}その理由は、多くの有用な機能や特性を静的に検証することが困難または不可能であるためです。たとえば、プログラムが A と B という 2 つの型を定義し、B が A のサブタイプであるとします。プログラムが型 A の値を型 B に変換しようとする場合（これはダウンキャストとして知られています）、変換される値が実際に型 B の値である場合にのみ、その操作は正当です。したがって、操作が安全であることを検証するために動的チェックが必要です。この要件は、ダウンキャストに対する批判の 1 つです。

定義上、動的型チェックは実行時にプログラムエラーを引き起こす可能性があります。一部のプログラミング言語では、これらのエラーを予測して回復することが可能ですが、他の言語では、型チェックエラーは致命的なエラーとみなされます。

動的型チェックは含むが静的型チェックは含まないプログラミング言語は、「動的型付けプログラミング言語」と呼ばれることが多い。

特定の言語では、静的型付けと動的型付けの両方が可能です。たとえば、Java やその他一見静的型付け言語に見える言語では、型をサブタイプにダウンキャストしたり、オブジェクトを照会して動的型を検出したり、実行時型情報に依存するその他の型操作をサポートしています。C ++ RTTIもその一例です。より一般的には、ほとんどのプログラミング言語には、非連結共用体、実行時多態性、バリアント型など、異なる「種類」のデータにディスパッチするためのメカニズムが含まれています。型注釈や型チェックと連携しない場合でも、このようなメカニズムは動的型付けの実装と実質的に類似しています。

オブジェクト指向言語におけるオブジェクトへのアクセスは、通常、静的ターゲット型（またはマニフェスト型）がオブジェクトの実行時型（潜在型）またはそのスーパー型のいずれかに等しい参照によって行われます。これは、特定の型のインスタンスに対して実行されるすべての操作は、サブタイプのインスタンスに対しても実行できるというリスコフの置換原理に準拠しています。この概念は、包含関係またはサブタイプ多態性としても知られています。一部の言語では、サブタイプは共変または反変の戻り値型および引数型を持つ場合もあります。

Clojure、Common Lisp、Cythonなどの特定の言語は、デフォルトでは動的型チェックが行われますが、オプションの注釈を提供することで、プログラムが静的型チェックを選択できるようにしています。このようなヒントを使用する理由の1つは、プログラムの重要なセクションのパフォーマンスを最適化することです。これは、段階的型付けによって形式化されています。Lispをベースとした教育環境であり、Racket言語の前身であるプログラミング環境DrRacketも、ソフト型付けです。^{[ 11 ]}

逆に、バージョン4.0以降、C#言語では変数を静的に型チェックしないことを示す方法が用意されています。型が の変数はdynamic静的型チェックの対象になりません。代わりに、プログラムは実行時の型情報に基づいて変数の使用方法を判断します。^{[ 12 ] [ 9 ] : 113–119}

Rustでは、トレイトオブジェクトは、ライフタイムを持たない、またはライフタイムのみを持つ型の動的型付けを提供します。^{[ 13 ]}dynstd::any::Any'static

静的型付けと動的型付けの選択には、一定のトレードオフが伴う。

静的型付けはコンパイル時に型エラーを確実に検出できるため、納品されるプログラムの信頼性が向上します。しかし、型エラーの発生頻度についてはプログラマの間で意見が分かれており、コード内で設計された型を適切に表現することで検出できるバグの割合についても意見が分かれています。^{[ 14 ] [ 15 ]}静的型付けの支持者は、プログラムが適切に型チェックされている場合に信頼性が高まると考えていますが、動的型付けの支持者は、信頼性が証明されている分散コードと小さなバグデータベースを指摘しています。静的型付けの価値は、型システムの強度が増すにつれて高まります。Dependent MLやEpigramなどの言語で実装されている依存型付けの支持者は、プログラムで使用される型がプログラマによって適切に宣言されているか、コンパイラによって正しく推論されている場合、ほとんどすべてのバグは型エラーとみなすことができると示唆しています。^{[ 16 ]}

静的型付けは通常、コンパイルされたコードの実行速度を向上させます。コンパイラが使用されている正確なデータ型を把握している場合（これは宣言または型推論による静的検証に必要）、最適化されたマシンコードを生成できます。Common Lispなどの一部の動的型付け言語では、この理由から最適化のためにオプションの型宣言が認められています。

対照的に、動的型付け言語では、ソースコードの変更によってチェックすべき箇所や再検討すべきコードが少なくなるため、コンパイラの実行速度が向上し、インタプリタが新しいコードを動的にロードできるようになる可能性がある。これもまた、編集・コンパイル・テスト・デバッグのサイクルを短縮する可能性がある。

型推論機能を持たない静的型付け言語（ C言語やJavaバージョン10以前など）では、プログラマがメソッドや関数が使用する型を宣言する必要があります。これは、静的なものではなく、アクティブで動的な追加のプログラムドキュメントとして機能します。これにより、コンパイラは同期がずれたり、プログラマに無視されたりするのを防ぐことができます。ただし、型宣言を必要とせずに静的型付けできる言語もあります（Haskell、Scala、OCaml、F#、Swift、そして程度は低いもののC#やC++など）。そのため、すべての言語で静的型付けに明示的な型宣言が必要なわけではありません。

動的型付けでは、単純な静的型チェックでは不正として拒否されるような構造も可能になります。例えば、任意のデータをコードとして実行するeval関数が実現可能になります。eval関数は静的型付けでも実現可能ですが、代数的データ型の高度な使用が必要です。さらに、動的型付けは、過渡的なコードやプロトタイピングにも適しており、例えば、完全なデータ構造の代わりにプレースホルダーデータ構造（モックオブジェクト）を透過的に使用できます（通常は実験やテストの目的で使用されます）。

動的型付けでは、一般的にダックタイピング（コードの再利用を容易にする手法）が利用できます。静的型付けを採用している言語の多くも、ダックタイピングやジェネリックプログラミングなどの仕組みを備えており、コードの再利用を容易にしています。

動的型付けは、一般的にメタプログラミングを容易にします。たとえば、C++ のテンプレートは、型定義 (関数と変数両方) に関するより厳格な規則があるため、同等のRubyやPythonコードよりも記述が煩雑になる傾向があります。そのため、開発者は、Python 開発者よりもテンプレートに対して多くの定型コードを記述する必要があります。メタクラスやイントロスペクションなどのより高度なランタイム構造は、静的型付け言語では使用しにくい場合が多いです。一部の言語では、このような機能を使用して、実行時データに基づいて、その場で新しい型や動作を生成することもできます。このような高度な構造は、動的プログラミング言語によって提供されることが多く、これらの言語の多くは動的型付けですが、動的型付けは必ずしも動的プログラミング言語と関連しているわけではありません。

プログラミング言語は、しばしば口語的に「強い型付け」または「弱い型付け」と呼ばれます。しかし実際には、これらの用語の意味について普遍的に受け入れられている定義はありません。一般的には、型システム間の違いを表すより正確な用語があり、それによって人々はそれらを「強い」または「弱い」と呼ぶのです。

プログラミング言語の型システムを分類する3つ目の方法は、型付き演算と型変換の安全性によるものです。コンピュータ科学者は、型システムの規則に違反する演算や型変換を許容しない言語を「型安全言語」と呼んでいます。

コンピュータ科学者は、プログラムが使用のために割り当てられていないメモリ領域にアクセスできない言語を「メモリ安全言語」（または単に「安全言語」）と呼びます。例えば、メモリ安全言語は配列の境界をチェックするか、あるいは静的に（つまり、実行前のコンパイル時に）配列の境界外へのアクセスがコンパイル時エラー、場合によっては実行時エラーを引き起こすことを保証します。

型安全かつメモリ安全である言語の次のプログラムを考えてみましょう。^{[ 17 ]}

var x := 5; 変数 y := "37"; var z := x + y; 

この例では、変数のz値は 42 になります。これはプログラマーが想定していた値ではないかもしれませんが、明確に定義された結果です。もしy別の文字列、つまり数値に変換できない文字列 (例: " Hello, World ") だったとしても、結果は同様に明確に定義されます。プログラムは型安全またはメモリ安全であっても、無効な操作でクラッシュすることがあります。これは、型システムがすべてのオペランドに対する操作の有効性を正確に指定できるほど高度ではない言語の場合です。しかし、プログラムが型安全でない操作に遭遇した場合、多くの場合、プログラムを終了させることが唯一の選択肢となります。

次に、C言語における同様の例を考えてみましょう。

int x = 5 ; char y [] = "37" ; char * z = x + y ; printf ( "%c \n " , * z );

この例ではz、 は の 5 文字先のメモリ アドレスを指します。これyは、 が指す文字列の終端ゼロ文字の 3 文字後に相当しますy。これは、プログラムがアクセスすることを想定していないメモリです。C 言語の用語では、これは単に未定義の動作であり、プログラムは何でも実行できます。単純なコンパイラでは、文字列 "37" の後に格納されているバイトを実際に出力するかもしれません。この例が示すように、C 言語はメモリセーフではありません。任意のデータが文字であると想定されているため、C 言語は型セーフな言語でもありません。

一般的に、型安全性とメモリ安全性は密接に関連しています。例えば、ポインタ演算と数値からポインタへの変換をサポートする言語（C言語など）は、任意のメモリをあたかも任意の型の有効なメモリであるかのようにアクセスできるため、メモリ安全性も型安全性も備えていません。

一部のプログラミング言語では、コードの異なる領域に異なるレベルのチェックを適用できます。例としては、以下のようなものがあります。

• JavaScript ^{[ 18 ] [ 19 ] [ 20 ]}およびPerluse strictのディレクティブは、より強力なチェックを適用します。
• PHP ^{[ 21 ]}declare(strict_types=1)では、ファイルごとに型宣言と完全に一致する型の変数のみが受け入れられ、そうでない場合は例外がスローされます。TypeError
• VB.NETのOption Strict Onを使用すると、コンパイラはオブジェクト間の変換を要求できます。

リンターやIBM Rational Purifyなどの追加ツールを使用することで、より高いレベルの厳密性を実現することもできます。

主にギラッド・ブラチャによって、型システムの選択は言語の選択とは独立して行われるべきであり、型システムは必要に応じて言語に組み込むことができるモジュールであるべきだと提案されている。彼は、強制型システムと呼ばれるものは言語の表現力を低下させ、コードをより脆弱にするため、これは有利だと考えている。^{[ 22 ]}型システムが言語の意味論に影響を与えないという要件を満たすのは難しい。

オプショナル型付けは、段階的型付けと関連していますが、それとは異なります。どちらの型付け方式もコードの静的解析（静的型付け）に使用できますが、オプショナル型システムは実行時に型安全性を強制しません（動的型付け）。^{[ 22 ] [ 23 ]}

依存型は、スカラーまたは値を使用して、他の値の型をより正確に記述するという考え方に基づいています。たとえば、${\displaystyle \mathrm {matrix} (3,3)}$おそらく、${\displaystyle 3\times 3}$行列。次に、行列の乗算に関する次のような型付け規則を定義できます。

${\displaystyle \mathrm {matrix} _{\mathrm {multiply} }:\mathrm {matrix} (k,m)\times \mathrm {matrix} (m,n)\to \mathrm {matrix} (k,n)}$

ここで、 k、m、nは任意の正の整数値です。この型システムに基づいてMLの派生版であるDependent MLが作成されましたが、従来の依存型の型チェックは決定不能であるため、それらを使用するすべてのプログラムを何らかの制限なしに型チェックできるわけではありません。Dependent ML は、決定できる等価性の種類をPresburger 算術に制限します。

Epigramなどの他の言語では、言語内のすべての式の値が決定可能であるため、型チェックも決定可能になります。しかし、一般に決定可能性の証明は決定不可能であるため、多くのプログラムでは非常に複雑な手書きの注釈が必要になります。これは開発プロセスを妨げるため、多くの言語実装では、この条件を無効にするオプションという形で簡単な解決策を提供しています。ただし、このオプションを使用すると、型チェックを行わないプログラムが入力された場合に型チェッカーが無限ループで実行され、コンパイルが失敗するという代償を伴います。

線形型は、線形論理の理論に基づき、一意性型と密接に関連しており、常に参照が1つしかないという特性を持つ値に割り当てられる型です。これらは、ファイルや文字列などの大きな不変値を記述するのに有用です。なぜなら、線形オブジェクトを破棄し、類似のオブジェクトを作成する操作（など）は、内部的にインプレース変異に最適化できるからです。通常、このような変異は、オブジェクトへの他の参照を保持しているプログラムの一部に副作用を引き起こし、参照透過性str = str + "a"を損なう可能性があるため、これは不可能です。また、プロトタイプオペレーティングシステムであるSingularityでは、プロセス間通信に使用され、プロセスが共有メモリ内のオブジェクトを共有できないように静的に保証することで、競合状態を防いでいます。Clean言語（Haskellに似た言語）は、この型システムを使用して、安全性を維持しながら（ディープコピーを実行する場合と比較して）大幅な速度向上を実現しています。

交差型とは、重複する値セットを持つ2つの型の両方に属する値を記述する型のことです。例えば、C言語のほとんどの実装では、符号付き文字型の範囲は-128から127、符号なし文字型の範囲は0から255です。したがって、これら2つの型の交差型の範囲は0から127になります。このような交差型は、符号付き文字型と符号なし文字型のどちらにも対応しているため、符号付き文字型または符号なし文字型のいずれかを期待する関数に安全に渡すことができます。

交差型は、オーバーロードされた関数型を記述するのに役立ちます。たとえば、「int→ int」が整数引数を受け取り整数を返す関数型であり、「float→ float」が浮動小数点引数を受け取り浮動小数点数を返す関数型である場合、これら2つの型の交差型を使用して、入力の型に応じてどちらか一方を実行する関数を記述できます。このような関数は、「int→ 」関数を期待する別の関数に安全に渡すことができ、単に「 → 」機能をint使用しないだけです。floatfloat

サブクラス化階層において、ある型と祖先型（親型など）の共通部分は、最も派生した型となる。兄弟型の共通部分は空である。

Forsythe言語には、交差型の一般的な実装が含まれています。限定された形式として、リファインメント型があります。

共用型は、2 つの型のいずれかに属する値を記述する型です。たとえば、C では、signed char の範囲は -128 から 127、unsigned char の範囲は 0 から 255 なので、これら 2 つの型の共用型は、アクセスする共用メンバーに応じて部分的に使用できる -128 から 255 の全体的な「仮想」範囲を持ちます。この共用型を扱う関数は、この完全な範囲の整数を扱う必要があります。より一般的には、共用型に対して有効な操作は、共用される両方の型に対して有効な操作のみです。C の「共用体」の概念は共用型に似ていますが、両方の型ではなくどちらか一方の型に対して有効な操作を許可するため、型安全ではありません。共用型は、正確な性質 (たとえば、値または型) が不明なシンボル値を表すために使用されるプログラム解析において重要です。

サブクラス階層において、ある型と祖先型（親型など）の和集合は祖先型となります。兄弟型の和集合は、それらの共通の祖先のサブタイプとなります（つまり、共通の祖先型で許可されているすべての操作は和集合型でも許可されますが、他にも共通の有効な操作が存在する場合があります）。

存在型は、実装とインターフェースを分離できるため、モジュールや抽象データ型を表すためにレコード型と組み合わせてよく使用されます。たとえば、型 "T = ∃X { a: X; f: (X → int); }" は、型Xのデータメンバaと、同じ型Xのパラメータを受け取り整数を返す関数fを持つモジュールインターフェースを表します。これは、たとえば次のように、さまざまな方法で実装できます。

• intT = { a: int; f: (int → int); }
• floatT = { a: float; f: (float → int); }

これらの型はどちらも、より一般的な存在型 T のサブタイプであり、具体的な実装型に対応しているため、これらの型のいずれかの値は型 T の値となります。型「T」の値「t」が与えられた場合、抽象型Xが何であっても、「tf(ta)」は型付けが適切であることが分かります。これにより、特定の実装に適した型を選択する際の柔軟性が確保される一方、インターフェース型（存在型）の値のみを使用するクライアントは、これらの選択から隔離されます。

一般的に、型チェッカーは、特定のモジュールがどの存在型に属するかを推論することはできません。上記の例では、intT { a: int; f: (int → int); } は、∃X { a: X; f: (X → int); } という型を持つ可能性もあります。最も簡単な解決策は、各モジュールに意図した型を注釈として付けることです。例:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

抽象データ型とモジュールはプログラミング言語にかなり前から実装されていましたが、1988年にジョン・C・ミッチェルとゴードン・プロトキンが「抽象[データ]型は存在型を持つ」というスローガンの下で形式理論を確立したのはそれ以降のことでした。^{[ 25 ]}この理論はSystem Fに似た2階型付きラムダ計算ですが、全称量化ではなく存在量化を使用しています。

段階的型付けの型システムでは、変数にはコンパイル時（静的型付け）または実行時（動的型付け）のいずれかで型を割り当てることができます。 ^{[ 26 ]}これにより、ソフトウェア開発者は単一の言語内で、必要に応じてどちらの型パラダイムも選択できます。^{[ 26 ]}段階的型付けでは、静的に未知の型を表すためにdynamicという特別な型を使用します。段階的型付けでは、型の等価性の概念を、 dynamic 型を他のすべての型に関連付けるconsistencyと呼ばれる新しい関係に置き換えます。この consistency 関係は対称ですが、推移的ではありません。^{[ 27 ]}