型理論

数学と理論計算機科学において、型理論とは特定の型システムの正式な表現である。^[a]型理論は型システムの学術的研究である。

いくつかの型理論は、数学の基礎として集合論の代替として機能します。基礎として提案されている 2 つの影響力のある型理論は次のとおりです。

• アロンゾ・チャーチの型付きλ計算
• ペル・マルティン＝レーフの直観主義型理論

コンピュータ化された証明記述システムのほとんどは、その基礎として型理論を使用しています。一般的な例としては、Thierry CoquandのCalculus of Inductive Constructionsがあります。

型理論は、素朴な集合論と形式論理に基づく数式のパラドックスを避けるために考案されました。ラッセルのパラドックス（ゴットロープ・フレーゲの『算術の基礎』で初めて説明）は、適切な公理がなければ、自分自身のメンバーではないすべての集合の集合を定義できるというものです。この集合は、自分自身を含み、また自分自身を含まないこともあります。1902年から1908年にかけて、バートランド・ラッセルはこの問題に対するさまざまな解決策を提案しました。

1908年までに、ラッセルは型の分岐理論と還元公理に到達し、これらは両方とも1910年、1912年、1913年に出版されたホワイトヘッドとラッセルの『プリンキピア・マテマティカ』に掲載された。この体系は、型の階層を作成し、具体的な数学的実体をそれぞれ特定の型に割り当てることで、ラッセルのパラドックスで示唆された矛盾を回避した。特定の型の実体は、その型のサブタイプのみで構築され、 ^{[b]実体がそれ自身を使って定義されることを防いだ。ラッセルのパラドックスのこの解決法は、}ツェルメロ-フランケル集合論などの他の形式体系で採用されているアプローチに似ている。^[3]

型理論は、アロンゾ・チャーチのラムダ計算との組み合わせで特に人気があります。型理論の初期の注目すべき例としては、チャーチの単純型付きラムダ計算があります。チャーチの型理論^[4]は、元の型なしラムダ計算を悩ませていたクリーネ・ロッサーのパラドックスを形式体系が回避するのに役立ちました。チャーチは^[c]これが数学の基礎として機能できることを実証し、高階論理と呼ばれました。

現代の文献では、「型理論」とは、ラムダ計算に基づく型付きシステムを指します。影響力のあるシステムの 1 つは、構成的数学の基礎として提案されたPer Martin-Löfの直観主義型理論です。もう 1 つは、Coq、Lean、およびその他のコンピューター証明アシスタントの基礎として使用されているThierry Coquandの構成計算です。型理論は活発な研究分野であり、1 つの方向性としてホモトピー型理論の開発があります。

最初のコンピュータ証明支援システムはオートマスと呼ばれ、型理論を使用してコンピュータ上で数学をエンコードしました。マーティン＝レーフは特に、すべての数学をエンコードして数学の新しい基礎となる直観主義型理論を開発しました。ホモトピー型理論を使用した数学の基礎に関する研究が進行中です。

圏論を研究する数学者はすでに、広く受け入れられているツェルメロ-フランケル集合論の基礎を扱うのに困難を抱えていました。このことが、ローヴェレの集合の圏の初等理論 (ETCS) などの提案につながりました。^{[6]ホモトピー型理論は、型理論を使用してこの方向を続けています。研究者は、従属型 (特に恒等型) と}代数的位相(特にホモトピー)の関係を研究しています。

型理論に関する現在の研究の多くは、証明チェッカー、対話型証明アシスタント、自動定理証明器によって推進されています。これらのシステムのほとんどは、証明をエンコードするための数学的基礎として型理論を使用していますが、型理論とプログラミング言語の密接な関係を考えると、これは驚くべきことではありません。

• LFはTwelfによって使用され、多くの場合他の型理論を定義します。
• 高階論理に属する多くの型理論は、HOL ファミリーの証明器とPVSによって使用されます。
• 計算型理論はNuPRLによって使用されます。
• 構成法とその導関数は、 Coq、Matita、Leanによって使用されます。
• UTT（Luoの依存型の統一理論）は、プログラミング言語と証明支援の両方であるAgdaで使用されています。

多くの型理論はLEGOとIsabelleによってサポートされています。Isabelle は、型理論以外にもZFCなどの基盤もサポートしています。Mizarは集合論のみをサポートする証明システムの例です。

コンパイラのセマンティック解析フェーズにおける型チェックアルゴリズムなどの静的プログラム解析はすべて、型理論と関係があります。代表的な例はAgdaです。これは、型システムに UTT (Luo の依存型の統一理論) を使用するプログラミング言語です。

プログラミング言語ML は型理論 ( LCFを参照) を操作するために開発され、その独自の型システムは型理論に大きく影響を受けました。

型理論は自然言語の意味論の形式理論にも広く使われており、^{[7] [8]、}特にモンタギュー文法^{[9]とその派生語に多く用いられている。特に}範疇文法と前群文法では、単語の型（名詞、動詞など）を定義するために型構成子を多用している。

最も一般的な構成は、それぞれ個体と真理値の基本型とを取り、型の集合を次のように再帰的に定義します。 ${\displaystyle e}$${\displaystyle t}$

• と が型であれば、 も型です。${\displaystyle a}$${\displaystyle b}$${\displaystyle \langle a,b\rangle }$
• 基本型と、前の節によってそれらから構築できるもの以外は何も型ではありません。

複合型は、型のエンティティから型のエンティティへの関数の型です。したがって、 のような型があり、これはエンティティから真理値への関数の集合、つまりエンティティの集合の指示関数の要素として解釈されます。 型の式は、エンティティの集合から真理値への関数、つまり集合の（指示関数）集合です。この後者の型は、 everyoneやnobodyのような自然言語量指定子の型であると標準的に考えられています（Montague 1973、Barwise and Cooper 1981）。^[10]${\displaystyle \langle a,b\rangle }$${\displaystyle a}$${\displaystyle b}$${\displaystyle \langle e,t\rangle }$${\displaystyle \langle \langle e,t\rangle ,t\rangle }$

レコード付き型理論は、レコードを使用して型理論の型を表現する形式的な意味論表現フレームワークです。これは自然言語処理、主に計算意味論や対話システムで使用されています。^{[11] [12]}

グレゴリー・ベイトソンは社会科学に論理型の理論を導入しました。彼のダブルバインドと論理レベルの概念はラッセルの型理論に基づいています。

型理論は数学的論理であり、つまり、判断を導く推論規則の集合である。ほとんどの論理には、「命題は真である」または「式は整形式の式である」と主張する判断がある。^[13]型理論には、型を定義し、それを項と呼ばれる形式オブジェクトの集合に割り当てる判断がある。項とその型は、しばしば と併せて記述される。 ${\displaystyle \varphi}$ ${\displaystyle \varphi}$${\displaystyle \mathrm {term} :{\mathsf {type}}}$

論理における項は、定数記号、変数、または関数適用（項が別の項に適用される）として再帰的に定義されます。定数記号には、自然数、ブール値、および後続関数や条件演算子などの関数が含まれます。したがって、項には、、、、などがあります。 ${\displaystyle 0}$${\displaystyle \mathrm {true} }$ ${\displaystyle \mathrm {S} }$ ${\displaystyle \mathrm {if} }$${\displaystyle 0}$${\displaystyle (\mathrm {S} \,0)}$${\displaystyle (\mathrm {S} \,(\mathrm {S} \,0))}$${\displaystyle (\mathrm {if} \,\mathrm {true} \,0\,(\mathrm {S} \,0))}$

ほとんどのタイプ理論には 4 つの判断があります。

• 「はタイプです」${\displaystyle T}$
• 「はタイプ「の用語です${\displaystyle t}$${\displaystyle T}$
• 「タイプはタイプに等しい」${\displaystyle T_{1}}$${\displaystyle T_{2}}$
• 「項と型の両方とも等しい」${\displaystyle t_{1}}$${\displaystyle t_{2}}$${\displaystyle T}$

判断は仮定から導かれることがあります。たとえば、「が 型の項であり、 が型の項であると仮定すると、が 型の項である」と言うことができます。このような判断は、正式にはターンスタイル記号で表されます。 ${\displaystyle x}$${\displaystyle {\mathsf {bool}}}$${\displaystyle y}$${\displaystyle {\mathsf {nat}}}$${\displaystyle (\mathrm {if} \,x\,y\,y)}$${\displaystyle {\mathsf {nat}}}$ ${\displaystyle \vdash}$

${\displaystyle x:{\mathsf {bool}},y:{\mathsf {nat}}\vdash ({\textrm {if}}\,x\,y\,y):{\mathsf {nat}}}$

仮定がなければ、改札口の左側には何もないでしょう。

${\displaystyle \vdash \mathrm {S} :{\mathsf {nat}}\to {\mathsf {nat}}}$

左側の仮定のリストは、判決の文脈です。 やなどの大文字のギリシャ文字は、仮定の一部またはすべてを表すためによく使用されます。したがって、4 つの異なる判決は通常、次のように記述されます。 ${\displaystyle \ガンマ}$${\displaystyle \Delta }$

いくつかの教科書では、これが判断的等価性であり、したがって等価性の外部概念であることを強調するために、3つの等号を使用しています。 ^[14]判断は、すべての用語に型があることを強制します。型によって、用語に適用できるルールが制限されます。 ${\displaystyle \equiv}$

型理論の推論規則は、他の判断の存在に基づいて、どのような判断ができるかを示します。規則は水平線を使用したゲンツェンスタイルの演繹として表現され、必要な入力判断は線の上に、結果として得られる判断は線の下にあります。^[15]たとえば、次の推論規則は、判断の等価性の置換規則を述べています。この規則は構文的で、を書き換えることで機能します。メタ変数、、、、、は、実際には単一のシンボルだけでなく、多くの関数適用を含む複雑な項と型で構成されている場合があります。 $${\displaystyle {\begin{array}{c}\Gamma \vdash t:T_{1}\qquad \Delta \vdash T_{1}=T_{2}\\\hline \Gamma ,\Delta \vdash t:T_{2}\end{array}}}$$ ${\displaystyle \ガンマ}$${\displaystyle \Delta }$${\displaystyle t}$${\displaystyle T_{1}}$${\displaystyle T_{2}}$

型理論で特定の判断を生成するには、それを生成する規則と、その規則に必要なすべての入力を生成する規則などが必要です。適用された規則は証明木を形成し、最上位の規則には仮定は必要ありません。入力を必要としない規則の 1 つの例は、定数項の型を述べる規則です。たとえば、型 の項が存在すると主張するには、次のように記述します。${\displaystyle 0}$${\displaystyle {\mathsf {nat}}}$$${\displaystyle {\begin{array}{c}\hline \vdash 0:nat\\\end{array}}}$$

一般的に、型理論の証明の望ましい結論は、型の居住の1つである。^[16]型の居住（と略記） の決定問題は次のとおりです。${\displaystyle \exists t.\Gamma \vdash t:\tau ?}$

コンテキストと型が与えられた場合、型環境内に型を割り当てることができる用語が存在するかどうかを判断します。${\displaystyle \ガンマ}$${\displaystyle \tau}$${\displaystyle t}$${\displaystyle \tau}$${\displaystyle \ガンマ}$

ジラールのパラドックスは、型の占有がカリー・ハワード対応による型システムの一貫性に強く関係していることを示しています。健全であるためには、そのようなシステムには占有されていない型がなければなりません。

型理論には通常、次のようないくつかのルールがあります。

• 判断を下す（この場合、文脈と呼ばれる）
• 文脈に仮定を加える（文脈の弱化）
• 仮定を組み替える
• 仮定を使用して変数を作成する
• 判断的平等性に対する反射性、対称性、推移性を定義する
• ラムダ項の適用のための置換を定義する
• 置換などの等価性の相互作用をすべてリストします
• タイプユニバースの階層を定義する
• 新しいタイプの存在を主張する

また、それぞれの「ルールによる」タイプには4種類のルールがあります。

• 「型形成」ルールは、型をどのように作成するかを示します
• 「用語導入」ルールは、「ペア」や「S」などの標準的な用語とコンストラクタ関数を定義します。
• 「項除去」ルールは、「first」、「second」、「R」などの他の関数を定義します。
• 「計算」ルールは、型固有の関数を使用して計算を実行する方法を指定します。

ルールの例については、興味のある読者はホモトピー型理論の本の付録A.2を参照するか、^[14] マルティン・レーフの直観主義型理論を読むとよいでしょう。^[17]

型理論の論理的枠組みは、直観主義論理、あるいは構成的論理に類似している。形式的には、型理論は、直観主義論理のブラウワー・ハイティング・コルモゴロフ解釈の実装としてよく引用される。^{[17]さらに、}カテゴリー理論やコンピュータプログラムとの関連も考えられる。

基礎として使用される場合、特定の型は命題（証明可能なステートメント）として解釈され、その型に存在する項はその命題の証明として解釈されます。いくつかの型が命題として解釈される場合、それらを接続して型からブール代数を作成するために使用できる共通の型のセットがあります。ただし、論理は古典論理ではなく直観論理であり、つまり排中律も二重否定もありません。

この直観主義的な解釈では、論理演算子として機能する一般的な型が存在します。

排中律は成立しないため、 型の項は存在しません。同様に、二重否定は成立しないため、 型の項は存在しません。 ${\displaystyle \Pi a.A+(A\to \bot )}$${\displaystyle \Pi A.((A\to \bot )\to \bot )\to A}$

排中律と二重否定を規則または仮定によって型理論に組み込むことは可能です。ただし、項は標準的な項まで計算されない可能性があり、2 つの項が判断的に等しいかどうかを判断する能力を妨げることになります。^[要出典]

ペル・マルティン＝レーフは、構成的数学の基礎として直観主義型理論を提唱した。^[13]構成的数学では、「特性 を持つ が存在する」ことを証明する場合、特定のと、それが特性 を持つことの証明を構築する必要がある。型理論では、存在は従属積型を使用して実現され、その証明にはその型の項が必要である。 ${\displaystyle x}$${\displaystyle P(x)}$${\displaystyle x}$${\displaystyle P}$

非構成的証明の例としては、背理法による証明がある。最初のステップは、が存在しないと仮定し、それを背理法によって反駁することである。そのステップからの結論は、「が存在しないということはあり得ない」である。最後のステップは、二重否定によって、が存在すると結論付けることである。構成的数学では、二重否定を除去してが存在すると結論付ける最後のステップは許可されない。^[18]${\displaystyle x}$${\displaystyle x}$${\displaystyle x}$${\displaystyle x}$

基礎として提案されている型理論のほとんどは構成的であり、証明支援系で使用されるもののほとんども含まれます。^[要出典]規則または仮定によって、型理論に非構成的な機能を追加することは可能です。これには、現在の継続での呼び出しなどの継続に対する演算子が含まれます。ただし、これらの演算子は、標準性やパラメトリック性などの望ましい特性を壊す傾向があります。

カリー・ハワード対応は、論理とプログラミング言語の間に見られる類似性です。論理における「A B」の含意は、型「A」から型「B」への関数に似ています。さまざまな論理において、ルールはプログラミング言語の型の式に似ています。類似性はさらに進み、ルールの適用はプログラミング言語のプログラムに似ています。したがって、この対応は「証明はプログラムである」と要約されることがよくあります。 ${\displaystyle \to}$

用語と型の対立は、実装と仕様の対立として見ることもできる。プログラム合成によって、（計算上の）型占有は、型情報の形で与えられた仕様からプログラム（全体または一部）を構築するために使用できる。^[19]

型理論を扱う多くのプログラム (対話型定理証明器など) は、型推論も行います。これにより、ユーザーの操作を少なくして、ユーザーが意図するルールを選択できます。

主要記事:圏論

カテゴリー理論の当初の動機は基礎主義からかけ離れていましたが、この 2 つの分野は深いつながりを持つことが判明しました。ジョン・レーン・ベルは次のように書いています。「実際、カテゴリーはそれ自体がある種の型理論とみなすことができます。この事実だけでも、型理論は集合論よりもカテゴリー理論に非常に密接に関連していることがわかります。」簡単に言えば、カテゴリーは、そのオブジェクトを型 (または種類) と見なすことによって型理論と見なすことができます。つまり、「大まかに言えば、カテゴリーは構文を取り除いた型理論と考えることができます。」このようにして、いくつかの重要な結果が導き出されます。^[20]

• デカルトの閉カテゴリは型付きλ計算（Lambek、1970）に対応する。
• C-モノイド（積と指数関数と 1 つの非終端オブジェクトを持つカテゴリ）は、型なし λ-計算（1980 年頃にLambek とDana Scottによって独立に観察された）に対応します。
• 局所的にデカルト的に閉じたカテゴリは、Martin-Löf 型理論(Seely, 1984)に対応します。

この相互作用はカテゴリカル論理として知られ、それ以来活発な研究の対象となっている。例えば、Jacobs (1999) のモノグラフを参照。

ホモトピー型理論は、型理論と圏論の融合を試みる。等式、特に型間の等式に焦点を当てる。ホモトピー型理論は、等式型の扱い方によって直観主義型理論と大きく異なる。2016年には、正規化を伴うホモトピー型理論である立方体型理論が提案された。^{[21] [22]}

最も基本的な型はアトムと呼ばれ、型がアトムである項はアトミック項と呼ばれます。型理論に含まれる一般的なアトミック項には、型 で表記されることが多い自然数、型 で表記されるブール論理値 ( / ) 、型が変化する可能性がある形式変数 などがあります。^[16]たとえば、次のようなものがアトミック項になります。 ${\displaystyle {\mathsf {nat}}}$${\displaystyle \mathrm {true} }$${\displaystyle \mathrm {false} }$${\displaystyle {\mathsf {bool}}}$

• ${\displaystyle 42:{\mathsf {nat}}}$
• ${\displaystyle \mathrm {true} :{\mathsf {bool}}}$
• ${\displaystyle x:{\mathsf {nat}}}$
• ${\displaystyle y:{\mathsf {bool}}}$

原子項に加えて、ほとんどの現代の型理論では関数も考慮されています。関数型は矢印記号を導入し、帰納的に定義されます。とが型である場合、表記は型のパラメータを受け取り、型の項を返す関数の型です。この形式の型は単純型として知られています。^[16]${\displaystyle \sigma}$${\displaystyle \tau}$${\displaystyle \sigma \to \tau }$${\displaystyle \sigma}$${\displaystyle \tau}$

いくつかの項は、次の項のように、単純な型を持つものとして直接宣言される場合があります。これは、2 つの自然数を順番に受け取り、1 つの自然数を返します。 ${\displaystyle \mathrm {追加} }$

${\displaystyle \mathrm {add} :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})}$

厳密に言えば、単純な型は1つの入力と1つの出力しか許さないので、上記の型をより忠実に読むと、 は自然数を取り込み、形式の関数を返す関数である、となります。括弧は、が型 を持たないことを明確に示しています。型 は、自然数の関数を取り、自然数を返す関数です。慣例的に矢印は右結合 であるため、の型から括弧を省略することができます。 ^[16]${\displaystyle \mathrm {add} }$${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$${\displaystyle \mathrm {add} }$${\displaystyle ({\mathsf {nat}}\to {\mathsf {nat}})\to {\mathsf {nat}}}$${\displaystyle \mathrm {add} }$

新しい関数項はラムダ式を使用して構築することができ、ラムダ項と呼ばれます。これらの項も帰納的に定義されます。ラムダ項は という形式を持ち、 は形式変数、 は項であり、その型は で表されます。 はの型、 はの型です。^[16]次のラムダ項は、入力された自然数を2倍にする関数を表します。 ${\displaystyle (\lambda v.t)}$${\displaystyle v}$${\displaystyle t}$${\displaystyle \sigma \to \tau }$${\displaystyle \sigma }$${\displaystyle v}$${\displaystyle \tau }$${\displaystyle t}$

${\displaystyle (\lambda x.\mathrm {add} \,x\,x):{\mathsf {nat}}\to {\mathsf {nat}}}$

変数は であり、（ラムダ項の型から暗黙的に）型 でなければなりません。項の型は であり、これは関数適用推論規則を 2 回適用することでわかります。したがって、ラムダ項の型は であり、これは自然数を引数として受け取り、自然数を返す関数であることを意味します。 ${\displaystyle x}$${\displaystyle {\mathsf {nat}}}$${\displaystyle \mathrm {add} \,x\,x}$${\displaystyle {\mathsf {nat}}}$${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$

ラムダ項は名前がないため、匿名関数と呼ばれることがよくあります^。匿名関数の概念は、多くのプログラミング言語に登場します。

型理論の力は、推論規則によって項がどのように組み合わせられるかを指定することにあります。^{[4]関数を持つ型理論には、}関数適用の推論規則もあります。が型の項であり、 が型の項である場合、の への適用(多くの場合 と表記されます) は型 を持ちます。たとえば、、、およびの型表記がわかっている場合、関数適用から次の型表記を演繹できます。^[16]${\displaystyle t}$${\displaystyle \sigma \to \tau }$${\displaystyle s}$${\displaystyle \sigma }$${\displaystyle t}$${\displaystyle s}$${\displaystyle (t\,s)}$${\displaystyle \tau }$${\displaystyle 0:{\textsf {nat}}}$${\displaystyle 1:{\textsf {nat}}}$${\displaystyle 2:{\textsf {nat}}}$

• ${\displaystyle (\mathrm {add} \,1):{\textsf {nat}}\to {\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,2)\,0):{\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,1)((\mathrm {add} \,2)\,0)):{\textsf {nat}}}$

括弧は演算の順序を示しますが、慣例により関数の適用は左結合であるため、必要に応じて括弧を省略することができます。^[16]上記の3つの例の場合、最初の2つでは括弧をすべて省略でき、3番目は と簡略化できます。 ${\displaystyle \mathrm {add} \,1\,(\mathrm {add} \,2\,0):{\textsf {nat}}}$

ラムダ項を許容する型理論には、-還元および-還元と呼ばれる推論規則も含まれる。これらは関数適用の概念をラムダ項に一般化する。記号的に、これらは次のように記述される。 ${\displaystyle \beta }$${\displaystyle \eta }$

• ${\displaystyle (\lambda v.t)\,s\rightarrow t[v\colon =s]}$（-削減）。${\displaystyle \beta }$
• ${\displaystyle (\lambda v.t\,v)\rightarrow t}$、が( -reduction )内の自由変数でない場合。${\displaystyle v}$${\displaystyle t}$${\displaystyle \eta }$

最初の簡約は、ラムダ項の評価方法を記述します。ラムダ式が項 に適用される場合、内のすべての を に置き換えます。2 番目の簡約は、ラムダ式と関数型の関係を明示的にします。 がラムダ項である場合、は に適用されているため関数項である でなければなりません。したがって、ラムダ式は と同等であり、どちらも 1 つの引数を受け取り、それに適用されます。^[4]${\displaystyle (\lambda v.t)}$${\displaystyle s}$${\displaystyle v}$${\displaystyle t}$${\displaystyle s}$${\displaystyle (\lambda v.t\,v)}$${\displaystyle t}$${\displaystyle v}$${\displaystyle t}$${\displaystyle t}$

たとえば、次の項は- 簡約される可能性があります。 ${\displaystyle \beta }$

${\displaystyle (\lambda x.\mathrm {add} \,x\,x)\,2\rightarrow \mathrm {add} \,2\,2}$

型と項の等価性の概念も確立する型理論では、対応する-等価性と-等価性の推論規則が存在する。^[16]${\displaystyle \beta }$${\displaystyle \eta }$

空の型には項がありません。型は通常、 または と記述されます。空の型の用途の 1 つは、型の占有の証明です。型 について、型 の関数を導出することが一貫している場合、 は占有されていません。つまり、項がありません。 ${\displaystyle \bot }$${\displaystyle \mathbb {0} }$${\displaystyle a}$${\displaystyle a\to \bot }$${\displaystyle a}$

ユニット型には、ちょうど 1 つの標準項があります。型はまたは と書かれ、単一の標準項は と書かれます。ユニット型は、型の居住の証明にも使用されます。型 について、型 の関数を導出することが一貫している場合、 は居住されており、つまり 1 つ以上の項を持っている必要があります。 ${\displaystyle \top }$${\displaystyle \mathbb {1} }$${\displaystyle \ast }$${\displaystyle a}$${\displaystyle \top \to a}$${\displaystyle a}$

ブール型には、正確に 2 つの標準用語があります。 型は通常、またはまたは と記述されます。 標準用語は通常、 およびです。 ${\displaystyle {\textsf {bool}}}$${\displaystyle \mathbb {B} }$${\displaystyle \mathbb {2} }$${\displaystyle \mathrm {true} }$${\displaystyle \mathrm {false} }$

自然数は通常、ペアノ算術のスタイルで実装されます。ゼロには標準的な用語があります。ゼロより大きい標準的な値は、後続関数の反復適用を使用します。 ${\displaystyle 0:{\mathsf {nat}}}$ ${\displaystyle \mathrm {S} :{\mathsf {nat}}\to {\mathsf {nat}}}$

一部の型理論では、関数やリストなどの複合項の型が引数の型に依存することが許されています。たとえば、型理論には依存型 があり、これは項のリストに対応し、各項は型 を持つ必要があります。この場合、は型 を持ち、 は理論内のすべての型の 集合を表します。${\displaystyle {\mathsf {list}}\,a}$${\displaystyle a}$${\displaystyle {\mathsf {list}}}$${\displaystyle U\to U}$${\displaystyle U}$

いくつかの理論では、型が型ではなく項に依存することも許可しています。たとえば、理論には型 があり、ここで はベクトルの長さをエンコードする型の項です。これにより、より詳細で型の安全性が高まります。ドット積などのベクトルの長さ制限や長さの一致要件を持つ関数は、この要件を型の一部としてエンコードできます。^[24]${\displaystyle {\mathsf {vector}}\,n}$${\displaystyle n}$${\displaystyle {\mathsf {nat}}}$

理論がどのような依存性が許容されるかについて注意を払わない場合、ジラールのパラドックスのような依存型から基礎的な問題が発生する可能性があります。論理学者ヘンク・バレンデグトは、依存型のさまざまな制限とレベルを研究するためのフレームワークとしてラムダキューブを導入しました。 ^[25]

積の型は 2 つの型に依存し、その項は一般に順序付きペア として、または記号 で表されます。 ペアの積の型はで、 はの型、は の型です。 積の型は通常、除去関数 および で定義されます。 ${\displaystyle (s,t)}$${\displaystyle \times }$${\displaystyle (s,t)}$${\displaystyle \sigma \times \tau }$${\displaystyle \sigma }$${\displaystyle s}$${\displaystyle \tau }$${\displaystyle t}$${\displaystyle \mathrm {first} :(\Pi \,\sigma \,\tau .\sigma \times \tau \to \sigma )}$${\displaystyle \mathrm {second} :(\Pi \,\sigma \,\tau .\sigma \times \tau \to \tau )}$

• ${\displaystyle \mathrm {first} \,(s,t)}$を返し、${\displaystyle s}$
• ${\displaystyle \mathrm {second} \,(s,t)}$を返します。${\displaystyle t}$

この型は、順序付きペアのほかに、論理積や論理積の概念にも使用されます。

和型は2つの型に依存し、通常は記号またはで記述されます。プログラミング言語では、和型はタグ付き共用体と呼ばれることがあります。型は通常、単射なコンストラクタおよびと、次のような エリミネータ関数で定義されます。${\displaystyle +}$${\displaystyle \sqcup }$${\displaystyle \sigma \sqcup \tau }$ ${\displaystyle \mathrm {left} :\sigma \to (\sigma \sqcup \tau )}$${\displaystyle \mathrm {right} :\tau \to (\sigma \sqcup \tau )}$${\displaystyle \mathrm {match} :(\Pi \,\rho .(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho )}$

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$を返し、${\displaystyle f\,x}$
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$を返します。${\displaystyle g\,y}$

和型は論理和と論理和の概念に使用されます。

2つの一般的な型依存性、従属積型と従属和型により、理論は全称量化と存在量化と同等のものとしてBHK直観主義論理をエンコードすることができます。これはカリー・ハワード対応によって形式化されています。^{[24]これらは}集合論の積と和にも関連しているため、それぞれ記号 と で表記されることがよくあります。[ ^17]従属積と和型は関数型によく現れ、プログラミング言語に頻繁に組み込まれています。^[26]${\displaystyle \Pi }$${\displaystyle \Sigma }$

たとえば、と型 の項を受け取り、末尾に要素があるリストを返す関数 を考えます。このような関数の型注釈は となり、「任意の型 に対して、と を渡し、 を返す」 と解釈できます。${\displaystyle \mathrm {append} }$${\displaystyle {\mathsf {list}}\,a}$${\displaystyle a}$${\displaystyle \mathrm {append} :(\Pi \,a.{\mathsf {list}}\,a\to a\to {\mathsf {list}}\,a)}$${\displaystyle a}$${\displaystyle {\mathsf {list}}\,a}$${\displaystyle a}$${\displaystyle {\mathsf {list}}\,a}$

和型は従属ペアで見られ、2 番目の型は最初の項の値に依存します。これは、関数が入力に基づいて異なるタイプの出力を返す可能性があるコンピューター サイエンスでは自然に発生します。たとえば、ブール型は通常、エリミネーター関数で定義され、3 つの引数を取り、次のように動作します。 ${\displaystyle \mathrm {if} }$

• ${\displaystyle \mathrm {if} \,\mathrm {true} \,x\,y}$を返し、${\displaystyle x}$
• ${\displaystyle \mathrm {if} \,\mathrm {false} \,x\,y}$を返します。${\displaystyle y}$

この関数の戻り値の型は入力によって異なります。型理論が依存型を許容する場合、次のような関数を定義することができます。 ${\displaystyle {\mathsf {bool}}}$${\displaystyle \mathrm {TF} \colon {\mathsf {bool}}\to U\to U\to U}$

• ${\displaystyle \mathrm {TF} \,\mathrm {true} \,\sigma \,\tau }$を返し、${\displaystyle \sigma }$
• ${\displaystyle \mathrm {TF} \,\mathrm {false} \,\sigma \,\tau }$を返します。${\displaystyle \tau }$

の型はと記述できます。 ${\displaystyle \mathrm {if} }$${\displaystyle (\Pi \,\sigma \,\tau .{\mathsf {bool}}\to \sigma \to \tau \to (\Sigma \,x:{\textsf {bool}}.\mathrm {TF} \,x\,\sigma \,\tau ))}$

カリー・ハワード対応の概念に従うと、恒等型は、型理論がすでに提供している 判断的（統語的）同値性ではなく、命題的同値性を反映するために導入された型です。

恒等型には同じ型の 2 つの項が必要で、記号 で記述されます。たとえば、と が項である場合、 は可能な型です。標準項は反射関数 で作成されます。項 の場合、 の呼び出しは型 に存在する標準項を返します。 ${\displaystyle =}$${\displaystyle x+1}$${\displaystyle 1+x}$${\displaystyle x+1=1+x}$${\displaystyle \mathrm {refl} }$${\displaystyle t}$${\displaystyle \mathrm {refl} \,t}$${\displaystyle t=t}$

型理論における等式の複雑さにより、これは活発な研究テーマとなっています。ホモトピー型理論は、主に型理論における等式を扱う注目すべき研究分野です。

帰納的型は、さまざまな型を作成するための一般的なテンプレートです。実際、上で説明したすべての型とそれ以上の型は、帰納的型のルールを使用して定義できます。帰納的型を生成する 2 つの方法は、帰納再帰と帰納帰納です。ラムダ項のみを使用する方法は、スコット エンコーディングです。

CoqやLeanなどの一部の証明支援システムは、帰納的型を持つ構造の計算である帰納的構造の計算に基づいています。

数学の最も一般的に受け入れられている基礎は、選択公理（略して ZFC）を伴うツェルメロ-フランケル集合論の言語と公理を伴う一階述語論理です。十分な表現力を持つ型理論も数学の基礎として機能する場合があります。これら 2 つのアプローチには多くの違いがあります。

• 集合論には規則と公理の両方があるが、型理論には規則のみがある。一般に、型理論には公理はなく、推論規則によって定義される。^[14]
• 古典的な集合論と論理学には排中律がある。型理論が「and」と「or」の概念を型としてコード化すると、直観主義論理につながり、必ずしも排中律を持つとは限らない。^[17]
• 集合論では、要素は 1 つの集合に限定されません。要素は、サブセットや他の集合との和集合に出現することができます。型理論では、項は (一般的に) 1 つの型にのみ属します。サブセットが使用される場合、型理論では述語関数を使用するか、依存型積型を使用します。この場合、各要素は、サブセットの特性が に対して成り立つという証明とペアになります。和集合が使用される場合、型理論では、新しい標準的な項を含む和型を使用します。${\displaystyle x}$${\displaystyle x}$
• 型理論には計算の概念が組み込まれています。したがって、「1+1」と「2」は型理論では異なる用語ですが、計算すると同じ値になります。さらに、関数は計算上、ラムダ項として定義されます。集合論では、「1+1=2」は、「1+1」が値「2」を参照する別の方法であることを意味します。型理論の計算には、複雑な等式の概念が必要です。
• 集合論は数を集合として符号化します。型理論は数をチャーチ符号化法を使って関数として符号化できますが、より自然には帰納的型として符号化することができ、その構成はペアノの公理によく似ています。
• 型理論では証明は型であるが、集合論では証明は基礎となる一階述語論理の一部である。^[14]

型理論の支持者は、 BHK解釈による構成的数学との関連、カリー・ハワード同型による論理との関連、そして圏論との関連も指摘するでしょう。

用語は通常、単一のタイプに属します。ただし、「サブタイプ」を定義する集合理論があります。

計算は、規則を繰り返し適用することによって行われます。多くの種類の理論は強く正規化されており、つまり、規則をどのような順序で適用しても、常に同じ結果になります。ただし、そうでない理論もあります。正規化タイプの理論では、一方向の計算規則は「削減規則」と呼ばれ、規則を適用すると項が「削減」されます。規則が一方向でない場合は、「変換規則」と呼ばれます。

いくつかの型の組み合わせは他の型の組み合わせと同等である。関数を「累乗」とみなすと、 型の組み合わせは代数的恒等式と同様に記述できる。^[26]したがって、、、、、。${\displaystyle {\mathbb {0} }+A\cong A}$${\displaystyle {\mathbb {1} }\times A\cong A}$${\displaystyle {\mathbb {1} }+{\mathbb {1} }\cong {\mathbb {2} }}$${\displaystyle A^{B+C}\cong A^{B}\times A^{C}}$${\displaystyle A^{B\times C}\cong (A^{B})^{C}}$

ほとんどの型理論には公理がありません。これは、型理論が推論規則によって定義されるためです。これは、理論が論理の推論規則 (一階述語論理など) と集合に関する公理の両方によって定義される集合論に精通している人にとっては混乱の原因となります。

場合によっては、型理論によっていくつかの公理が追加されます。公理とは、推論規則を使用した導出なしに受け入れられる判断です。多くの場合、公理は、規則では明確に追加できないプロパティを保証するために追加されます。

公理は、その項を計算する方法がない項を導入すると問題を引き起こす可能性があります。つまり、公理は型理論の正規化特性を妨げる可能性があります。 ^[27]

よく見られる公理は次のとおりです。

• 「公理K」は「同一性証明の一意性」を保証する。つまり、同一性型のすべての項は反射性と等しい。^[28]
• 「普遍性公理」は、型の同値性は型の等価性であると主張している。この性質の研究は立方体型理論につながり、公理を必要とせずにこの性質が成り立つようになった。^[22]
• 「排中律」は、直観主義論理ではなく古典論理を求めるユーザーを満足させるために追加されることが多いです。

選択公理は、ほとんどの型理論では推論規則から導出できるため、型理論に追加する必要はありません。これは、値が存在することを証明するには、その値を計算する方法が必要となる、型理論の構成的性質によるものです。選択公理は、型理論の関数が計算可能でなければならず、構文駆動型であるため、型内の項の数が数えられなければならないため、ほとんどの集合論ほど強力ではありません。(選択公理 § 構成的数学を参照。)

• 単純に型付けされたラムダ計算は高階論理である
• 直観主義型理論
• システムF
• LFは他の型理論を定義するためによく使われる
• 構成法とその導関数の計算

• オートマス
• ST型理論
• UTT (Luo の依存型の統一理論)
• いくつかの組み合わせ論理
• ラムダキューブで定義されているもの（純粋型システムとも呼ばれる）
• 型付きラムダ計算という名前で呼ばれる他のもの

• ホモトピー型理論は型の等価性を探求する
• 立方体型理論はホモトピー型理論の実装である。

• クラス（集合論）
• 論理
• タイプとトークンの区別

• 多くのトピックに関する記事が掲載されている nLab の型理論。
• スタンフォード哲学百科事典の直観主義型理論の記事
• Henk Barendregt 著の「ラムダ計算と型」の本
• ヘルムート・ブランドルによる構築の微積分 / 型付きラムダ微積分の教科書スタイルの論文
• Per Martin-Löf による直観主義型理論ノート
• Martin-Löf の型理論の本におけるプログラミング
• ホモトピー型理論を数学的基礎として提唱した本。

• Robert L. Constable (編)。「計算型理論」。Scholarpedia。
• TYPES フォーラム — 1987 年から運営されている、コンピュータ サイエンスの型理論に焦点を当てたモデレートされた電子メール フォーラムです。
• Nuprl ブック:「型理論入門」
• タイプ 2005～2008 年夏期講習プロジェクト講義ノート
  • 2005年のサマースクールでは入門講義が行われます
• オレゴンプログラミング言語サマースクール、多数の講義といくつかのメモ。
  • 2013年夏の講義（ロバート・ハーパーのYouTubeでの講演を含む）
  • 2015 年夏 型、論理、意味論、検証
• アンドレイ・バウアーのブログ