型システム

コンピュータプログラミングにおいて、型システムとは、型と呼ばれる特性（例えば、整数、浮動小数点、文字列）をあらゆる用語（単語、句、またはその他の記号セット）に割り当てる一連の規則からなる論理システムである。通常、用語は変数、式、関数、モジュールなど、コンピュータプログラムのさまざまな言語構成要素である。^[1]型システムは、用語に対して実行できる操作を指示する。変数の場合、型システムはその用語の許容値を決定する。

型システムは、プログラマが代数データ型、データ構造、またはその他のデータ型（「文字列」、「浮動小数点の配列」、「ブール値を返す関数」など）に使用する暗黙のカテゴリを形式化し、強制します。

型システムは、多くの場合、プログラミング言語の一部として指定され、インタープリタやコンパイラに組み込まれますが、言語の型システムは、言語の元の型構文と文法を使用して追加のチェックを実行するオプションのツールによって拡張できます。

プログラミング言語における型システムの主な目的は、型エラーによるコンピュータプログラムのバグの可能性を減らすことです。^[2]型エラーを構成するものは特定の型システムによって決まりますが、一般的には、特定の種類の値を期待する操作が、その操作が意味をなさない値で使用されるのを防ぐことが目的です（妥当性エラー）。

型システムを使用すると、コンピュータ プログラムのさまざまな部分間のインターフェイスを定義し、それらの部分が一貫した方法で接続されているかどうかを確認できます。このチェックは、静的 (コンパイル時)、動的 (実行時)、またはその両方の組み合わせで実行できます。

型システムには、ビジネスルールを表現する、特定のコンパイラ最適化を有効にする、複数のディスパッチを許可する、ドキュメントの形式を提供するなどの他の目的もあります。

単純な型システムの例としては、C 言語の型システムがあります。C プログラムの部分は関数定義です。1 つの関数は別の関数によって呼び出されます。

関数のインターフェースは、関数の名前と、関数のコードに渡されるパラメータのリストを示します。呼び出し関数のコードには、呼び出される関数の名前と、それに渡す値を保持する変数の名前が示されます。

コンピュータ プログラムの実行中、値は一時記憶域に配置され、その後、呼び出された関数のコードに実行がジャンプします。呼び出された関数のコードは値にアクセスし、それらを利用します。

関数内の命令が整数値を受け取ることを前提として記述されているが、呼び出しコードが浮動小数点値を渡した場合、呼び出された関数によって間違った結果が計算されます。

C コンパイラは、関数が呼び出されたときに関数に渡される引数の型を、関数の定義で宣言されたパラメータの型と比較します。型が一致しない場合、コンパイラはコンパイル時エラーまたは警告をスローします。

コンパイラは、値の静的型を使用して、必要なストレージと値の操作アルゴリズムの選択を最適化することもできます。多くのCコンパイラでは、たとえばfloat データ型は、単精度浮動小数点数の IEEE 仕様に従って32ビットで表現されます。そのため、これらの値には浮動小数点固有のマイクロプロセッサ操作(浮動小数点の加算、乗算など) が使用されます。

型制約の深さとその評価方法は、言語の型付けに影響します。プログラミング言語は、型多態性の場合、さらに操作を各型のさまざまな解決に関連付けることがあります。型理論は、型システムの研究です。整数や文字列など、一部のプログラミング言語の具体的な型は、コンピューター アーキテクチャ、コンパイラの実装、言語設計の実際的な問題に依存します。

正式には、型理論は型システムを研究します。プログラミング言語は、コンパイル時または実行時に、手動で注釈を付けるか自動的に推論するかに関係なく、型システムを使用して型チェックを行う機会を持たなければなりません。マーク・マナセは簡潔に次のように述べています。^[3]

型理論が取り組む基本的な問題は、プログラムが意味を持つことを保証することです。型理論によって生じる基本的な問題は、意味のあるプログラムに意味が与えられていない可能性があるということです。より豊富な型システムの探求は、この緊張から生じます。

データ型を割り当てること（型付け）は、メモリ内の値や変数などのオブジェクトなどのビットのシーケンスに意味を与えます。汎用コンピュータのハードウェアは、たとえばメモリアドレスと命令コード、または文字、整数、浮動小数点数を区別することができません。これは、ビットのシーケンスが意味する可能性のある値の間で本質的な区別がないためです。^{[注 1]}ビットのシーケンスを型に関連付けると、その意味がプログラム可能なハードウェアに伝達され、そのハードウェアと何らかのプログラムで構成される記号システムが形成されます。

プログラムは各値を少なくとも 1 つの特定の型に関連付けますが、1 つの値が多くのサブタイプに関連付けられることもあります。オブジェクト、モジュール、通信チャネル、依存関係などの他のエンティティも、型に関連付けられることがあります。型も型に関連付けられることがあります。型システムの実装では、理論上、データ型(値の型)、クラス(オブジェクトの型)、種類(型の型、またはメタタイプ) と呼ばれる識別情報を関連付けることができます。これらは、システムに含まれるレベルの階層で型付けが通過できる抽象化です。

プログラミング言語がより複雑な型システムを開発すると、基本的な型チェックよりもきめ細かいルール セットが得られますが、型推論(およびその他のプロパティ) が決定不能になり、プログラマーがコードに注釈を付けたり、コンピューター関連の操作や機能を考慮したりするためにより多くの注意を払う必要があるという代償が伴います。型安全な方法ですべてのプログラミング プラクティスを満たす、十分に表現力のある型システムを見つけるのは困難です。

プログラミング言語コンパイラは、依存型または効果システムを実装することもできます。これにより、さらに多くのプログラム仕様を型チェッカーで検証できます。単純な値と型のペアを超えて、コードの仮想「領域」は、何で何が行われているかを説明する「効果」コンポーネントに関連付けられ、たとえばエラーレポートを「スロー」できるようになります。したがって、シンボリックシステムは型と効果のシステムである可能性があり、これにより、型チェックのみの場合よりも多くの安全性チェックが可能になります。

コンパイラによって自動化されているか、プログラマによって指定されているかに関係なく、型システムは、型システムのルールから外れるとプログラムの動作を不正にします。プログラマが指定した型システムの利点は次のとおりです。

• 抽象化(またはモジュール性) - 型により、プログラマーは低レベルの実装に煩わされることなく、ビットやバイトよりも高いレベルで考えることができます。たとえば、プログラマーは文字列を単なるバイトの配列としてではなく、文字値のセットとして考え始めることができます。さらに高いレベルでは、型により、プログラマーは任意のサイズの2 つのサブシステム間のインターフェイスについて考え、表現することができます。これにより、より多くのレベルのローカリゼーションが可能になり、サブシステムの相互運用性に必要な定義は、それらの 2 つのサブシステムが通信するときに一貫性が保たれます。
• ドキュメント– より表現力豊かな型システムでは、型はプログラマーの意図を明確にするドキュメントの形式として機能します。たとえば、プログラマーが関数をタイムスタンプ型を返すものとして宣言した場合、タイムスタンプ型がコードのより深い部分で整数型として明示的に宣言できる場合、関数がドキュメント化されます。

コンパイラ指定の型システムによって得られる利点は次のとおりです。

• 最適化– 静的型チェックは、コンパイル時に役立つ情報を提供する場合があります。たとえば、型によって値がメモリ内で 4 バイトの倍数に揃えられる必要がある場合、コンパイラはより効率的なマシン命令を使用できる可能性があります。
• 安全性– 型システムにより、コンパイラは意味のないコードや無効なコードを検出できます。たとえば、3 / "Hello, World"規則で整数を文字列で割る方法が指定されていない場合、式を無効として識別できます。強い型付けは安全性を高めますが、完全な型の安全性を保証することはできません。

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

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

型の制約を検証および適用するプロセス (型チェック) は、コンパイル時(静的チェック) または実行時(動的チェック) に発生する場合があります。

言語仕様が型付け規則を強く要求し、情報を失わない自動型変換のみを許可する場合、そのプロセスを強く型付けされたプロセスと呼ぶことができます。そうでない場合は、弱く型付けされたプロセスと呼ぶことができます。

これらの用語は通常、厳密な意味では使用されません。

静的型チェックは、プログラムのテキスト (ソース コード)の分析に基づいてプログラムの型の安全性を検証するプロセスです。プログラムが静的型チェッカーに合格した場合、そのプログラムはすべての可能な入力に対していくつかの型の安全性プロパティ セットを満たすことが保証されます。

静的型チェックは、限定された形式のプログラム検証(型安全性を参照) と見なすことができ、型安全な言語では最適化と見なすこともできます。コンパイラがプログラムの型が適切であることを証明できる場合、動的安全性チェックを発行する必要がなく、結果として得られるコンパイル済みバイナリはより高速に実行され、サイズも小さくなります。

チューリング完全な言語の静的型チェックは本質的に保守的です。つまり、型システムが健全（つまり、すべての誤ったプログラムを拒否する）かつ決定可能（つまり、プログラムが適切に型付けされているかどうかを判断するアルゴリズムを記述できる）である場合、その型システムは不完全（つまり、実行時エラーが発生しないにもかかわらず拒否される正しいプログラムが存在する）である必要があります。^[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]その理由は、多くの有用な機能やプロパティは静的に検証することが困難または不可能であるためです。たとえば、プログラムが 2 つの型 A と B を定義し、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]dyn std::any::Any'static

静的型付けと動的型付けの選択には、一定のトレードオフが必要です。

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

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

対照的に、動的型付けでは、コンパイラの実行速度が向上し、インタープリタが新しいコードを動的にロードできるようになります。これは、動的型付け言語のソース コードを変更すると、実行するチェックが少なくなり、再確認するコードが少なくなるためです。^{[説明が必要]}これによっても、編集、コンパイル、テスト、デバッグのサイクルが短縮される可能性があります。

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

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

動的型付けでは通常、ダックタイピング（コードの再利用を容易にする）が可能です。静的型付けを備えた多くの^[指定]言語では、ダックタイピングや、コードの再利用を容易にするジェネリックプログラミングなどの他のメカニズムも採用されています。

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

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

プログラミング言語の型システムを分類する 3 番目の方法は、型付けされた操作と変換の安全性です。コンピューター科学者は、型システムのルールに違反する操作や変換を許可しない言語を表すために、型安全言語という用語を使用します。

コンピュータ科学者は、メモリセーフ言語(または単にセーフ言語)という用語を使用して、プログラムが、その使用のために割り当てられていないメモリにアクセスすることを許可しない言語を表します。たとえば、メモリセーフ言語は配列の境界をチェックするか、配列の境界外の配列アクセスがコンパイル時エラー、場合によっては実行時エラーを引き起こすことを静的に保証します (つまり、実行前のコンパイル時に)。

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

var x := 5;   
var 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 文字後に相当します。これは、プログラムがアクセスすることが想定されていないメモリです。C の用語では、これは単に未定義の動作であり、プログラムは何でも行うことができます。単純なコンパイラでは、文字列 "37" の後に格納されているバイトを実際に印刷する可能性があります。この例が示すように、C はメモリ セーフではありません。任意のデータが文字であると想定されているため、C は型セーフな言語でもありません。 y

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

詳細については、「メモリの安全性」を参照してください。

一部の言語では、コードのさまざまな領域にさまざまなレベルのチェックを適用できます。例:

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

より高いレベルの厳密性を実現するために、 lintやIBM Rational Purifyなどの追加ツールも使用できます。

主にギラッド・ブラチャによって、型システムの選択は言語の選択とは独立して行われるべきであると提案されている。つまり、型システムは必要に応じて言語にプラグインできるモジュールであるべきだというものである。彼は、これが有利だと考えている。なぜなら、彼が強制型システムと呼ぶものは言語の表現力を低下させ、コードをより脆弱にするからである。^[22]型システムが言語のセマンティクスに影響を与えないという要件を満たすのは困難である。

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

ポリモーフィズムという用語は、コード (特に関数やクラス) が複数の型の値に対して動作できること、または同じデータ構造の異なるインスタンスが異なる型の要素を含むことができることを指します。ポリモーフィズムを許可する型システムは、通常、コードの再利用性を高めるためにそれを行います。ポリモーフィズムのある言語では、プログラマーはリストや連想配列などのデータ構造を1 回実装するだけで済みます。使用する予定の要素の型ごとに 1 回実装する必要はありません。このため、コンピューター サイエンティストは、特定の形式のポリモーフィズムの使用をジェネリック プログラミングと呼ぶことがあります。ポリモーフィズムの型理論的基礎は、抽象化、モジュール性、および (場合によっては)サブタイピングの基礎と密接に関連しています。

特定のデータタイプを持つ特定の環境での使用や、帯域外の静的プログラム分析に特化した型システムが数多く作成されています。多くの場合、これらは正式な型理論のアイデアに基づいており、プロトタイプ研究システムの一部としてのみ利用可能です。

次の表は、特殊な型システムで使用される型理論の概念の概要を示しています。M 、N、Oという名前は用語の範囲に及び、名前は型の範囲に及びます。次の表記法が使用されます。 ${\displaystyle \sigma ,\tau }$

• ${\displaystyle M:\sigma }$はタイプ であることを意味します。${\displaystyle M}$${\displaystyle \sigma}$
• ${\displaystyle M(N)}$のアプリケーションです。${\displaystyle M}$${\displaystyle N}$
• ${\displaystyle \tau [\alpha :=\sigma ]}$(それぞれ)は、型変数α (それぞれ項変数x )のすべての出現を型σ (それぞれ項N )に置き換えた結果として得られる型を表します。${\displaystyle \tau [x:=N]}$${\displaystyle \tau}$

依存型は、スカラーまたは値を使用して他の値の型をより正確に記述するという考え方に基づいています。たとえば、行列の型が考えられます。次に、行列の乗算に関する次の規則のような型付け規則を定義できます。 ${\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は任意の正の整数値です。 Dependent MLと呼ばれるMLの変種は、この型システムに基づいて作成されていますが、従来の依存型の型チェックは決定不可能であるため、それらを使用するすべてのプログラムが何らかの制限なしに型チェックできるわけではありません。 Dependent ML は、決定できる等式の種類をプレスブルガー算術に制限します。

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

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

交差型は、重複する値セットを持つ 2 つの他の型の両方に属する値を記述する型です。たとえば、C のほとんどの実装では、signed char の範囲は -128 から 127 で、unsigned char の範囲は 0 から 255 であるため、これら 2 つの型の交差型の範囲は 0 から 127 になります。このような交差型は、両方の型と互換性があるため、signed char または unsigned char のいずれかを期待する関数に安全に渡すことができます。

交差型は、オーバーロードされた関数型を記述する場合に便利です。たとえば、「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: (int → int); } を持つこともできます。最も簡単な解決策は、すべてのモジュールに意図した型を注釈付けすることです。例:

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

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

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

C や Java などの静的型システムの多くは、型宣言を必要とします。つまり、プログラマーは各変数を特定の型に明示的に関連付ける必要があります。Haskell などの他のシステムでは、型推論が実行されます。つまり、コンパイラーは、プログラマーが変数をどのように使用するかに基づいて、変数の型について結論を導きます。たとえば、とを加算する関数がある場合、加算は数値に対してのみ定義されているため、コンパイラーは、とが数値でなければならないと推論できます。したがって、プログラム内の他の場所で、引数として数値以外の型 (文字列やリストなど) を指定する呼び出しを行うと、エラーが発生します。 f(x, y)xyxyf

コード内の数値定数や文字列定数、式は、特定のコンテキストで型を暗示することがあります。たとえば、式は浮動小数点3.14の型を暗示する場合がありますが、 は整数のリスト (通常は配列)を暗示する場合があります。 [1, 2, 3]

型推論は、それが問題の型システムで計算可能であれば、一般に可能です。さらに、特定の型システムで一般に推論が計算可能でなくても、現実世界のプログラムの大部分では推論が可能な場合がよくあります。Haskell の型システムはHindley–Milnerのバージョンであり、 System Fωをいわゆるランク 1 多態型に制限したもので、型推論が計算可能です。ほとんどの Haskell コンパイラは、拡張として任意ランクの多態性を許可していますが、これにより型推論が計算可能ではなくなります。(ただし、型チェックは決定可能であり、ランク 1 プログラムには依然として型推論があります。明示的な型注釈が与えられない限り、より高いランクの多態型プログラムは拒否されます。)

型付け規則を使用して型環境内の用語に型を割り当てる型システムは、当然のことながら、型チェック、型可能性、型の占有などの決定問題と関連している。^[28]

• 型環境、用語、型が与えられた場合、型環境内で用語に型を割り当てることができるかどうかを判断します。${\displaystyle \Gamma }$${\displaystyle e}$${\displaystyle \tau }$${\displaystyle e}$${\displaystyle \tau }$
• 用語 が与えられた場合、型環境と型が存在し、その用語に型環境 内の型を割り当てることができるかどうかを判断します。${\displaystyle e}$${\displaystyle \Gamma }$${\displaystyle \tau }$${\displaystyle e}$${\displaystyle \tau }$${\displaystyle \Gamma }$
• 型環境と型が与えられた場合、型環境内に型を割り当てることができる項が存在するかどうかを判断します。${\displaystyle \Gamma }$${\displaystyle \tau }$${\displaystyle e}$${\displaystyle \tau }$

C#やScalaなどの言語には、統一された型システムがあります。^{[29]これは、プリミティブ型を含むすべての}C#型が単一のルートオブジェクトから継承されることを意味します。C #のすべての型はObjectクラスから継承されます。JavaやRakuなどの一部の言語にはルート型がありますが、オブジェクトではないプリミティブ型もあります。^[30] Javaは、プリミティブ型と一緒に存在するラッパーオブジェクト型を提供するため、開発者はラッパーオブジェクト型またはより単純な非オブジェクトプリミティブ型のどちらかを使用できます。Rakuは、メソッドがアクセスされると、プリミティブ型をオブジェクトに自動的に変換します。^[31]

静的に型付けされた言語の型チェッカーは、任意の式の型が、その式が出現するコンテキストで想定される型と一致しているかどうかを検証する必要があります。たとえば、という形式の代入文では、式の推論された型は、変数 の宣言された型または推論された型と一致している必要があります。この一貫性の概念は互換性と呼ばれ、各プログラミング言語に固有のものです。 x := eex

の型eと の型xが同じで、その型に代入が許可されている場合、これは有効な式です。したがって、最も単純な型システムでは、2 つの型に互換性があるかどうかという問題は、それらが等しい(または同等) かどうかという問題に帰着します。ただし、言語が異なれば、2 つの型式が同じ型を表すと理解される基準も異なります。これらの異なる型の等式理論は大きく異なり、2 つの極端なケースは、同じ構造を持つ値を記述する任意の 2 つの型が同等である構造型システムと、構文的に異なる 2 つの型式が同じ型を表すことはない (つまり、型が同等であるためには、同じ「名前」を持つ必要がある) 名詞型システムです。

サブタイプ化のある言語では、互換性関係はより複雑です。Bが のサブタイプである場合A、 型の値は、B型の 1 つが期待されるコンテキストで使用できますA(共変)。ただし、その逆は当てはまりません。 等価性と同様に、サブタイプ関係はプログラミング言語ごとに定義が異なり、さまざまなバリエーションが可能です。 言語にパラメトリックまたはアドホックな多態性が存在すると、型の互換性にも影響が出る可能性があります。

• 型システムの比較
• 共変性と反変性（コンピュータサイエンス）
• オブジェクト指向プログラミングにおけるポリモーフィズム
• 型シグネチャ
• 型理論

• Cardelli , Luca ; Wegner, Peter (1985年12 月)。「型、データ抽象化、およびポリモーフィズムの理解について」(PDF)。ACM Computing Surveys。17 ( 4): 471–523。CiteSeerX 10.1.1.117.695。doi : 10.1145 / 6041.6042。S2CID  2921816。 
• ピアス、ベンジャミン C. (2002)。型とプログラミング言語。MIT プレス。ISBN 978-0-262-16209-8。
• Cardelli, Luca (2004)。「型システム」(PDF)。Allen B. Tucker (編)。CRCコンピュータサイエンスおよびエンジニアリングハンドブック(第 2 版)。CRC プレス。ISBN 978-1584883609。
• Tratt, Laurence (2009 年 7 月)。「5 .動的型付け言語」。Advances in Computers。第 77 巻。Elsevier。pp. 149–184。doi :10.1016/S0065-2458(09) 01205-4。ISBN 978-0-12-374812-6。

Wikibook Adaプログラミングには、型に関するページがあります。

Wikibook Haskellにはクラス宣言に関するページがあります。

• ウィキメディア・コモンズの型システムに関連するメディア
• Smith, Chris (2011)。「型システムについて議論する前に知っておくべきこと」。