型システム

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

プログラミング言語では型システムは、変数関数モジュールなど、コンピュータプログラムのさまざまな構成要素にと呼ばれるプロパティを割り当てる一連のルールで構成される論理システムです。[1]これらの型は、プログラマーが代数的データ型、データ構造、またはその他のコンポーネント( "string"、 "array of float"、 "function return boolean"など)に使用する暗黙のカテゴリーを形式化して適用します。型システムの主な目的は、バグの可能性を減らすことですコンピュータプログラム[2]では、コンピュータプログラムのさまざまな部分の間のインターフェイスを定義し、それらの部分が一貫した方法で接続されていることを確認します。このチェックは、静的(コンパイル時)、動的(実行時)、または両方の組み合わせとして実行できます。型システムには、ビジネスルールの表現、特定のコンパイラの最適化の有効化、複数のディスパッチの許可、ドキュメントの形式の提供 など、他の目的もあります。

型システムは、型を各計算値に関連付け、これらの値のフローを調べることにより、型エラーが発生しないことを確認または証明しようとします。問題の特定の型システムは、何が型エラーを構成するかを決定しますが、一般に、目的は、特定の種類の値を期待する操作が、その操作が意味をなさない値(有効性エラー)で使用されないようにすることです。型システムは、プログラミング言語の一部として指定され、インタープリターとコンパイラーに組み込まれることがよくありますが、言語の型システムは、言語の元の型構文と文法を使用して追加のチェックを実行 するオプションのツールによって拡張できます。

使用方法の概要

単純型システムの例は、C言語のシステムです。Cプログラムの部分は関数定義です。ある関数が別の関数によって呼び出されます。関数のインターフェースは、関数の名前と関数のコードに渡されるパラメーターのリストを示します。呼び出し元の関数のコードは、呼び出された関数の名前と、それに渡される値を保持する変数の名前を示します。実行中、値は一時ストレージに配置され、実行は呼び出された関数のコードにジャンプします。呼び出された関数のコードは値にアクセスし、それらを利用します。関数内の命令が整数値を受け取ることを前提として記述されているが、呼び出し元のコードが浮動小数点値の場合、呼び出された関数によって間違った結果が計算されます。Cコンパイラーは、関数が呼び出されたときに関数に渡される引数のタイプを、関数の定義で宣言されたパラメーターのタイプと照合します。タイプが一致しない場合、コンパイラはコンパイル時エラーをスローします。

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

タイプ制約の深さとその評価方法は、言語のタイピングに影響を与えます。プログラミング言語は、タイプポリモーフィズム場合、操作をタイプごとにさまざまな解像度にさらに関連付けることができます。型理論は型システムの研究です。整数や文字列など、一部のプログラミング言語の具体的なタイプは、コンピューターアーキテクチャ、コンパイラの実装、および言語設計の実際的な問題によって異なります。

基礎

正式には、型理論は型システムを研究します。プログラミング言語には、コンパイル時または実行時、手動で注釈を付けるか、自動的に推測するかにかかわらず、型システムを使用して型チェックを行う機会が必要です。マーク・マナスが簡潔に述べているように:[ 3]

型理論が取り組む根本的な問題は、プログラムに意味があることを確認することです。型理論によって引き起こされる根本的な問題は、意味のあるプログラムがそれらに帰する意味を持たないかもしれないということです。より豊かな型システムの探求は、この緊張から生じます。

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

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

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

コンパイラーによって課される型制限が多いほど、プログラミング言語はより強く型付けされます。強く型付けされた言語では、暗黙の変換が害を及ぼさない状況で、プログラマーが明示的な変換を行う必要があることがよくあります。Pascalの型システムは、たとえば、配列または文字列のサイズがその型の一部であり、一部のプログラミングタスクを困難にするため、「強すぎる」と説明されています。[4] [5] Haskellも強く型付けされていますが、その型は自動的に推測されるため、明示的な変換は不要なことがよくあります。

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

コンパイラーによって自動化されているか、プログラマーによって指定されているかにかかわらず、型システムは、型システムの規則の範囲外である場合、プログラムの動作を違法にします。プログラマー指定の型システムによって提供される利点は次のとおりです。

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

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

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

タイプエラー

タイプエラーは、プログラム開発の複数の段階で現れる可能性のある意図しない状態[説明が必要]です。したがって、型システムにはエラーを検出するための機能が必要です。型推論が自動化されているHaskellなどの一部の言語では、エラーの検出を支援するために、コンパイラーが lintを使用できる場合があります。

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

タイプチェック

タイプの制約を検証および適用するプロセス(タイプチェック)は、コンパイル時(静的チェック)または実行時に発生する可能性があります言語仕様がその型付け規則を強く要求する場合(つまり、情報を失わない自動型変換のみを多かれ少なかれ許可する場合)、プロセスを強く型付けされたものとして、そうでない場合は弱く型付けされたものとして参照できます。これらの用語は通常、厳密な意味で使用されることはありません。

静的型チェック

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

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

チューリング完全言語の静的型チェックは本質的に保守的です。つまり、型システムが健全(すべての誤ったプログラムを拒否することを意味する)であり、決定可能(プログラムが適切に型付けされているかどうかを判断するアルゴリズムを記述できることを意味する)である場合、それは不完全である必要があります(正しいプログラムであり、ランタイムエラーが発生していなくても拒否されます)。[6]たとえば、次のコードを含むプログラムについて考えてみます。

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

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

ダウンキャストなど、多くの便利で一般的なプログラミング言語機能を静的にチェックすることはできませんしたがって、多くの言語には静的型と動的型の両方のチェックがあります。静的型チェッカーはそれが何ができるかを検証し、動的チェックは残りを検証します。

静的型チェックを備えた多くの言語は、型チェッカーをバイパスする方法を提供します。一部の言語では、プログラマーは静的型と動的型の安全性を選択できます。たとえば、C#は、静的に型付けされた変数と動的に型付けされた変数を区別します。前者の使用は静的にチェックされますが、後者の使用は動的にチェックされます。他の言語では、タイプセーフではないコードを書くことができます。たとえば、Cでは、プログラマーは同じサイズの任意の2つの型の間で値を自由にキャストでき、型の概念を効果的に覆すことができます。

静的型チェックを使用する言語のリストについては、静的型付き言語のカテゴリーを参照してください。

動的型チェックと実行時型情報

動的型チェックは、実行時にプログラムの型安全性を検証するプロセスです。動的に型チェックされる言語の実装は、通常、各ランタイムオブジェクトを、その型情報を含む型タグ(つまり、型への参照)に関連付けます。この実行時型情報(RTTI)は、動的ディスパッチ遅延バインディングダウンキャストリフレクション、および同様の機能 を実装するためにも使用できます。

ほとんどのタイプセーフ言語には、静的タイプチェッカーもある場合でも、何らかの形式の動的タイプチェックが含まれています。[要出典] [8]この理由は、多くの有用な機能またはプロパティを静的に検証することが困難または不可能であるためです。たとえば、プログラムがAとBの2つのタイプを定義するとします。ここで、BはAのサブタイプです。プログラムがタイプAの値をタイプBに変換しようとする場合、これはダウンキャストと呼ばれ、操作は有効です。変換される値が実際にタイプBの値である場合。したがって、操作が安全であることを確認するために動的チェックが必要です。この要件は、ダウンキャストに対する批判の1つです。

定義上、動的型チェックにより、実行時にプログラムが失敗する可能性があります。一部のプログラミング言語では、これらの障害を予測して回復することが可能です。その他の場合、タイプチェックエラーは致命的と見なされます。

静的型チェックを含まない動的型チェックを含むプログラミング言語は、「動的型付けプログラミング言語」と呼ばれることがよくあります。このような言語のリストについては、動的型付けプログラミング言語のカテゴリーを参照してください。

静的型チェックと動的型チェックの組み合わせ

一部の言語では、静的型付けと動的型付けの両方が可能です。たとえば、Javaやその他の表面上静的に型付けされた言語は、サブタイプへの型のダウンキャストをサポートし、オブジェクトにクエリを実行して、実行時型情報に依存する動的型やその他の型操作を検出します。別の例はC ++ RTTIです。より一般的には、ほとんどのプログラミング言語には、非交和実行時ポリモーフィズムバリアント型など、さまざまな「種類」のデータをディスパッチするためのメカニズムが含まれています型注釈や型チェックを操作しない場合でも、このようなメカニズムは動的型付けの実装と実質的に似ています。プログラミング言語を見る静的型付けと動的型付けの間の相互作用の詳細については。

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

ClojureCommon LispCythonなどの特定の言語は、デフォルトで動的に型チェックされますが、オプションの注釈を提供することにより、プログラムが静的型チェックを選択できるようにします。このようなヒントを使用する理由の1つは、プログラムのクリティカルセクションのパフォーマンスを最適化することです。これは、漸進的型付けによって形式化されます。プログラミング環境DrRacket、Lispに基づく教育環境、および言語Racketの前身もソフトタイプです。[9]

逆に、バージョン4.0の時点では、C#言語は、変数を静的に型チェックしてはならないことを示す方法を提供します。dynamic型が静的型チェックの対象とならない変数。代わりに、プログラムは実行時型情報に依存して、変数の使用方法を決定します。[10]

Rustでは型は型の動的型付けを提供します。[11]std::any'static

実際の静的および動的型チェック

静的型付けと動的型付けのどちらを選択するかには、特定のトレードオフが必要です。

静的型付けは、コンパイル時に型エラーを確実に検出できるため、提供されるプログラムの信頼性が向上します。ただし、プログラマーは、型エラーがどの程度一般的に発生するかについて意見が分かれており、設計された型をコードで適切に表現することで検出される、コード化されたバグの割合についてさらに意見が分かれます。[12] [13]静的型付けの支持者[誰?]動的型付けの支持者[誰?]信頼できることが証明されている分散コードと小さなバグデータベースを指します。[要出典]静的型付けの値は、型システムの強度が増すにつれて増加します。依存型の支持者[誰?] Dependent MLEpigramなどの言語で実装されているため、プログラムで使用される型がプログラマーによって適切に宣言されているか、コンパイラーによって正しく推測されている場合、ほとんどすべてのバグが型エラーと見なされる可能性があります。[14]

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

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

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

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

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

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

強い型と弱い型システム

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

型安全性とメモリ安全性

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

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

タイプセーフとメモリセーフの両方を備えた言語の次のプログラムについて考えてみます。[15]

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 ); 

この例では、5文字を超えるメモリアドレスを指します。これは、が指す文字列の終了ゼロ文字の後の3文字に相当しますこれは、プログラムがアクセスすることを期待されていないメモリです。ガベージデータが含まれている可能性があり、確かに有用なものは含まれていません。この例が示すように、Cはメモリセーフでもタイプセーフでもありません。 zyy

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

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

型チェックの可変レベル

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

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

lintIBMRational Purifyなどの追加ツールを使用して、より高いレベルの厳密性を実現することもできます。

オプション型システム

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

オプション型付けは漸進的型付けに関連していますが、漸進的型付けとは異なります。両方の型付け分野を使用してコードの静的分析を実行できますが(静的型付け)、オプションの型システムは実行時に型の安全性を強制しません(動的型付け)。[20] [21]

ポリモーフィズムと型

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

特殊型システム

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

次の表は、特殊な型システムで使用される型理論の概念の概要を示しています。名前M、N、Oは、用語と名前にまたがっていますタイプの範囲。表記(または)は、 τ内の型変数α(または項変数x)のすべての出現をσ(または項Nで置き換えた結果として生じる型を記述します。

タイプの概念 表記 意味
関数 Mにタイプがある場合Nのタイプはσであり、アプリケーションはタイプτです。
製品 Mにタイプがある場合、 それからは、 NのタイプがσOのタイプがτであるようなペアです。
Mにタイプがある場合、次にどちらかNがタイプσであるような最初の注入である、または

Nがタイプτを持つような2回目の単射です。

交差点 Mにタイプがある場合MのタイプはσMのタイプはτです。
連合 Mにタイプがある場合MはタイプσまたはMはタイプτです。
記録 Mにタイプがある場合Mには、タイプτのメンバーxがあります。
多形 Mにタイプがある場合Mはタイプ任意のタイプσに対して。
実存的 Mにタイプがある場合Mはタイプあるタイプのσの場合。
再帰的 Mにタイプがある場合Mはタイプ
依存関数 Mにタイプがある場合Nのタイプはσであり、アプリケーションはタイプがあります
依存製品 Mにタイプがある場合、 それからNのタイプがσOのタイプがタイプのペアです。
従属交差点[22] Mにタイプがある場合MはタイプσMはタイプ
家族の交差点[22] Mにタイプがある場合Mはタイプタイプσの任意の項Nに対して。
家族組合[22] Mにタイプがある場合Mはタイプタイプσのある項Nに対して。

依存型

依存型は、スカラーまたは値を使用して他の値の型をより正確に記述するという考えに基づいています。例えば、のタイプかもしれませんマトリックス。次に、行列の乗算に関する次のルールなどの入力ルールを定義できます。

ここで、kmnは任意の正の整数値です。この型システムに基づいて、依存型MLと呼ばれるMLのバリアントが作成されましたが、従来の依存型の型チェックは決定不可能であるため、それらを使用するすべてのプログラムが何らかの制限なしに型チェックできるわけではありません。依存MLは、プレスバーガー算術に決定できる等式の種類を制限します

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

線形タイプ

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

交差型

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

交差型は、オーバーロードされた関数型を記述するのに役立ちます。たとえば、「」が整数引数を取り、整数を返す関数の型であり、「」がfloat引数を取り、floatを返す関数の型である場合、これらの2つのタイプの共通部分を使用して、与えられた入力のタイプに基づいて、どちらか一方を実行する関数を記述することができます。このような関数は、「 → 」関数を安全に期待する別の関数に渡すことができます。単に「」機能を使用しません。 intintfloatfloatintintfloatfloat

サブクラス化階層では、型と祖先型(その親など)の共通部分が最も派生した型です。兄弟タイプの共通部分は空です。

Forsythe言語には、交差型の一般的な実装が含まれています。制限された形式は、改良タイプです。

共用体タイプ

共用体型は、2つの型のいずれかに属する値を記述する型です。たとえば、Cでは、signed charの範囲は-128〜127であり、unsigned charの範囲は0〜255であるため、これら2つのタイプの和集合は、全体的な「仮想」範囲が-128〜255になります。アクセスされるユニオンメンバーに応じて部分的に使用されます。この共用体型を処理する関数は、この完全な範囲の整数を処理する必要があります。より一般的には、共用体タイプで有効な操作は、結合されている両方のタイプで有効な演算のみです。Cの「共用体」の概念は共用体型に似ていますが、両方ではなくどちらかの型で有効な操作を許可するため、型セーフではありませ共用体タイプは、プログラム分析で重要です。共用体タイプは、正確な性質(値やタイプなど)が不明なシンボリック値を表すために使用されます。

サブクラス化階層では、型と祖先型(その親など)の和集合が祖先型です。兄弟タイプの和集合は、共通の祖先のサブタイプです(つまり、共通の祖先で許可されているすべての操作は、共用体タイプで許可されますが、他の有効な操作も共通している場合があります)。

存在型

存在型は、実装をインターフェースから分離できるため、モジュールおよび抽象データ型を表すためにレコード型に関連して頻繁に使用されます。たとえば、タイプ "T =∃X{a:X; f:(X→int);}"は、タイプXaという名前のデータメンバーと同じタイプXで、​​整数を返します。これはさまざまな方法で実装できます。例えば:

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

これらの型は両方とも、より一般的な存在型Tのサブ型であり、具体的な実装型に対応します。したがって、これらの型のいずれかの値は、型Tの値です。型「T」の値「t」が与えられると、「 tf(ta) "は、抽象型Xが何であるかに関係なく、適切に型指定されています。これにより、特定の実装に適したタイプを柔軟に選択できますが、インターフェイスタイプ(既存のタイプ)の値のみを使用するクライアントは、これらの選択から分離されます。

一般に、タイプチェッカーが特定のモジュールが属する既存のタイプを推測することは不可能です。上記の例では、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年のことでした。[23]理論は、システムFに似た2次型付きラムダ計算ですが、全称記号ではなく実存的定量化を使用しています。

漸進的型付け

漸進的型付けは、コンパイル時(静的型付け)または実行時(動的型付け)のいずれかで変数に型を割り当てることができる型システムであり、ソフトウェア開発者は内部から必要に応じていずれかの型パラダイムを選択できます。単一の言語。[24]特に、漸進的型付けは、動的という名前の特別な型を使用して静的に未知の型を表し、漸進的型付けは、型の同等性の概念を、動的型を他のすべての型に関連付ける一貫性と呼ばれる新しい関係に置き換えます。整合性の関係は対称的ですが、推移的ではありません。[25]

明示的または暗黙的な宣言と推論

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

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

問題の型システムで計算可能であれば、型推論は一般的に可能です。さらに、特定の型システムで一般に推論が計算できない場合でも、実際のプログラムの大部分で推論が可能であることがよくあります。Hindley-MilnerのバージョンであるHaskellの型システムは、型推論が計算可能な、いわゆるランク1ポリモーフィック型へのシステムFωの制限です。ほとんどのHaskellコンパイラは、拡張機能として任意のランクのポリモーフィズムを許可しますが、これにより型推論が計算できなくなります。(ただし、型チェックは決定可能ですが、ランク1のプログラムには型推論があります。明示的な型注釈が与えられていない限り、上位のポリモーフィックプログラムは拒否されます。)

決定問題

型規則を使用して型環境の用語に型を割り当てる型システムは、当然、型チェック型付け可能性、および型居住の決定問題関連付けられています。[26]

  • 与えられたタイプの環境、 用語、およびタイプ、用語かどうかを決定しますタイプを割り当てることができますタイプ環境で。
  • 与えられた用語、型環境が存在するかどうかを判断しますとタイプそのような用語タイプを割り当てることができますタイプ環境で
  • 与えられたタイプの環境とタイプ、用語が存在するかどうかを判断しますタイプを割り当てることができますタイプ環境で。

統一型システム

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

互換性:同等性とサブタイピング

静的に型付けされた言語の型チェッカーは、式の型が、その式が表示されるコンテキストで予期される型と一致していることを確認する必要がありますたとえば、形式の代入ステートメントでは、式の推定型は、変数の宣言型または推定型と一致している必要があります互換性と呼ばれるこの一貫性の概念は、各プログラミング言語に固有のものです。 x := eex

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

サブタイピングのある言語では、互換性の関係はより複雑です。特に、Bがのサブタイプである場合、その逆が真でない場合でも、タイプAの値は、タイプの1つが期待されるBコンテキスト(共変)で使用できます。同等性と同様に、サブタイプの関係はプログラミング言語ごとに異なる方法で定義され、多くのバリエーションが可能です。言語 にパラメトリックまたはアドホック多相が存在することも、型の互換性に影響を与える可能性があります。A

も参照してください

メモ

  1. ^ Burroughs ALGOLコンピュータラインは、フラグビットによってメモリ位置の内容を決定しました。フラグビットは、メモリ位置の内容を指定します。命令、データ型、および機能は、48ビットの内容に加えて3ビットのコードで指定されます。MCP(マスター制御プログラム)のみがフラグコードビットに書き込むことができました。

参考文献

  1. ^ Pierce 2002、p。1:「型システムは、計算する値の種類に従ってフレーズを分類することにより、特定のプログラムの動作がないことを証明するための扱いやすい構文方法です。」
  2. ^ Cardelli 2004、p。1:「型システムの基本的な目的は、プログラムの実行中に実行エラーが発生しないようにすることです。」
  3. ^ Pierce 2002、p。208。
  4. ^ タイソン、JR(1983年4月25日)。「JRTは彼が有罪だと言っています—使用可能なパスカルを作成したことについて」Infoworld5、いいえ。1.p。66。
  5. ^ カーニハン、ブライアン(1981)。「なぜPascalは私のお気に入りのプログラミング言語ではないのですか」2012年4月6日にオリジナルからアーカイブされました2011年10月22日取得
  6. ^ 「...音の決定可能な型システムは不完全でなければなりません」—D。レミー(2017)。p。29、レミー、ディディエ。「プログラミング言語の型システム」(PDF)2013年5月26日取得
  7. ^ ピアス2002
  8. ^ Gaurav Miglani、Gaurav(2018)。「Javaでの動的メソッドディスパッチまたはランタイムポリモーフィズム」2020年12月7日にオリジナルからアーカイブされました2021-03-28を取得
  9. ^ ライト、アンドリューK.(1995)。実用的なソフトタイピング(PhD)。ライス大学。hdl1911/16900
  10. ^ "動的(C#リファレンス)"MSDNライブラリMicrosoft 2014年1月14日取得
  11. ^ "std :: any —Rust"doc.rust-lang.org 2021-07-07を取得
  12. ^ マイヤー、エリック; ドレイトン、ピーター。「可能な場合は静的型付け、必要な場合は動的型付け:プログラミング言語間の冷戦の終結」(PDF)マイクロソフトコーポレーション。
  13. ^ ラウチャー、アマンダ; ちなみに、ポール(2012)。「タイプとテスト」InfoQ。
  14. ^ Xi、Hongwei(1998)。実用的なプログラミング(PhD)の依存型。カーネギーメロン大学数理科学部。CiteSeerX10.1.1.41.548_ 
    Xi、Hongwei; Pfenning、Frank(1999)。「実用的なプログラミングにおける依存型」。プログラミング言語の原理に関する第26回ACMSIGPLAN-SIGACTシンポジウムの議事録ACM。pp。214–227。CiteSeerX10.1.1.69.2042 _ 土井10.1145 /292540.292560ISBN 1581130953S2CID245490 _
  15. ^ Visual Basicは、タイプセーフとメモリセーフの両方を備えた言語の例です。
  16. ^ 「4.2.2ECMAScriptの厳密なバリアント」ECMAScript®2020言語仕様(第11版)。ECMA。2020年6月。ECMA-262。
  17. ^ 「厳密モード–JavaScript」MDNDeveloper.mozilla.org。2013-07-03 2013年7月17日取得
  18. ^ 「厳密モード(JavaScript)」MSDNMicrosoft 2013年7月17日取得
  19. ^ 「厳密な型付け」PHPマニュアル:言語リファレンス:関数
  20. ^ a b Bracha、G。「PluggableTypes」(PDF)
  21. ^ 「もちろんです。これは「漸進的型付け」と呼ばれ、流行と見なします。...」静的型付けと動的型付けの両方を可能にする言語はありますか?スタックオーバーフロー。2012年。
  22. ^ a b c Kopylov、Alexei(2003)。「依存交差:型理論でレコードを定義する新しい方法」。コンピュータサイエンスにおける論理に関する第18回IEEEシンポジウムLICS2003。IEEEComputerSociety。pp。86–95。CiteSeerX10.1.1.89.4223_ 土井10.1109 /LICS.2003.1210048 
  23. ^ ミッチェル、ジョンC。; プロトキン、ゴードンD.(1988年7月)。「抽象型には存在型がある」(PDF)ACMTrans。プログラム。ラング。Syst10(3):470–502。土井10.1145 /44501.45065S2CID1222153_  
  24. ^ ジーク、ジェレミー(2014年3月24日)。「漸進的型付けとは何ですか?」
  25. ^ ジーク、ジェレミー; タハ、ワリド(2006年9月)。関数型言語の漸進的型付け(PDF)スキームと関数型プログラミング2006シカゴ大学pp。81–92。
  26. ^ バレンドレッグ、ヘンク; デッカーズ、ウィル; スタットマン、リチャード(2013年6月20日)。タイプのラムダ計算ケンブリッジ大学出版局。p。66. ISBN 978-0-521-76614-2
  27. ^ 「8.2.4型システムの統合」。C#言語仕様(第5版)。ECMA。2017年12月。ECMA-334。
  28. ^ 「ネイティブタイプ」Perl6ドキュメント
  29. ^ 「数値、§自動ボクシング」Perl6ドキュメント

さらに読む

外部リンク