従属型

コンピュータサイエンスと論理学において、依存型とは定義が値に依存する型のことである。これは型理論と型システムの重複する特徴である。直観主義型理論では、依存型は「すべてに対して」や「存在する」などの論理の量指定子をエンコードするために使用される。Agda 、ATS、Coq、F*、Epigram、Idris、Leanなどの関数型プログラミング 言語では、依存型はプログラマが可能な実装のセットをさらに制限する型を割り当てることを可能にすることでバグを減らすのに役立つ。

依存型の一般的な例としては、依存関数と依存ペアの 2 つがあります。依存関数の戻り値の型は、引数の 1 つの値(型だけでなく)によって異なる場合があります。たとえば、正の整数を取る関数は長さ の配列を返すことがあります。この場合、配列の長さは配列の型の一部です。(これは、型を引数として含むポリモーフィズムやジェネリック プログラミングとは異なることに注意してください。) 依存ペアには 2 番目の値がある場合があり、その型は最初の値によって異なります。配列の例を続けると、依存ペアは、型安全な方法で配列とその長さをペアにするために使用できます。 ${\displaystyle n}$${\displaystyle n}$

依存型は型システムに複雑さを追加します。プログラム内の依存型の等価性を決定するには計算が必要になる場合があります。依存型に任意の値が許可されている場合、型の等価性を決定するには、2つの任意のプログラムが同じ結果を生成するかどうかを決定することが必要になる場合があります。したがって、型チェックの決定可能性は、特定の型理論の等価性の意味、つまり型理論が内包的か外延的かによって異なります。^[1]

1934年、ハスケル・カリーは、型付きラムダ計算とその組み合わせ論理の対応物で使用される型が、命題論理の公理と同じパターンに従っていることに気付きました。さらに、論理のすべての証明に対して、プログラミング言語に一致する関数（項）がありました。カリーの例の1つは、単純型付きラムダ計算と直観主義論理の対応でした。^[2]

述語論理は命題論理の拡張であり、量指定子を追加します。ハワードとデ・ブリュインは、ラムダ計算を拡張して、このより強力な論理に一致させ、「すべてに対して」に対応する従属関数の型と、「存在する」に対応する従属ペアを作成しました。^[3]

このこととハワードの他の研究により、命題を型として扱うことはカリー・ハワード対応として知られています。

大まかに言えば、依存型は、インデックス付きの集合の族の型に似ています。より正式には、型の集合内の型が与えられた場合、各項に型を割り当てる型の族を持つことができます。型はによって変化すると言います。 ${\displaystyle A:{\mathcal {U}}}$${\displaystyle {\mathcal {U}}}$ ${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle a:A}$${\displaystyle B(a):{\mathcal {U}}}$${\displaystyle B(a)}$${\displaystyle a}$

戻り値の型が引数によって変化する関数（つまり、固定の共役領域がない関数）は従属関数と呼ばれ、この関数の型は従属積型、π型（Π型）、または従属関数型と呼ばれます。^[4]型の族から、項が内の項を取り項を返す関数である従属関数の型を構築できます。この例では、従属関数型は通常、またはと記述されます。 ${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \prod _{x:A}B(x)}$${\displaystyle a:A}$${\displaystyle B(a)}$${\textstyle \prod _{x:A}B(x)}$${\textstyle \prod {(x:A)}B(x)}$

が定数関数である場合、対応する従属積型は通常の関数型と同等です。つまり、が に依存しない場合、 はと判断的に等しくなります。 ${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \prod _{x:A}B}$${\displaystyle A\to B}$${\displaystyle B}$${\displaystyle x}$

「Π 型」という名前は、これらが型の直積として見られるという考えに由来しています。Π 型は、全称量指定子のモデルとしても理解できます。

たとえば、実数のn組について と書くと、 は、自然数nが与えられると、サイズnの実数の組を返す関数の型になります。通常の関数空間は、範囲型が実際には入力に依存しない特別なケースとして発生します。たとえば、 は自然数から実数への関数の型であり、型付きラムダ計算では と記述されます。 ${\displaystyle \operatorname {Vec} (\mathbb {R} ,n)}$${\textstyle \prod _{n:\mathbb {N} }\operatorname {Vec} (\mathbb {R} ,n)}$ ${\textstyle \prod _{n:\mathbb {N} }{\mathbb {R} }}$${\displaystyle \mathbb {N} \to \mathbb {R} }$

より具体的な例として、 を0 から 255 までの符号なし整数 (8 ビットまたは 1 バイトに収まるもの) の型とし、を とすると、は の積になります。 ${\displaystyle A}$${\displaystyle B(a)=X_{a}}$${\displaystyle a:A}$${\textstyle \prod _{x:A}B(x)}$${\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}$

従属積型の 双対は、従属ペア型、従属和型、シグマ型、または（紛らわしいですが）従属積型です。^[4]シグマ型は存在量指定子として理解することもできます。上記の例を続けると、型の宇宙に型と型のファミリーがある場合、従属ペア型が存在します。（代替表記はΠ型と同様です。） ${\displaystyle {\mathcal {U}}}$${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\textstyle \sum _{x:A}B(x)}$

従属ペア型は、2番目の項の型が最初の項の値に依存する順序付きペアの考え方を捉えたものである。 の場合、かつとなる。 が定数関数の場合、従属ペア型は積型、つまり通常の直積となる（判断的に等しい）。^[4]${\textstyle (a,b):\sum _{x:A}B(x),}$${\displaystyle a:A}$${\displaystyle b:B(a)}$${\displaystyle B}$${\displaystyle A\times B}$

より具体的な例として、 を再び 0 から 255 までの符号なし整数の型とし、 を再び256 以上の任意の に対して と等しくすると、 は合計 になります。 ${\displaystyle A}$${\displaystyle B(a)}$${\displaystyle X_{a}}$${\displaystyle X_{a}}$${\textstyle \sum _{x:A}B(x)}$${\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}$

を何らかの型とし、 とします。Curry-Howard 対応により、 はの項に関する論理述語として解釈できます。 が与えられた場合、型に人が住んでいるかどうかは、 がこの述語を満たすかどうかを示します。 この対応は存在量化と従属ペアに拡張できます。つまり、命題は型に人が住んでいる場合にのみ真です。 ${\displaystyle A:{\mathcal {U}}}$${\displaystyle B:A\to {\mathcal {U}}}$${\displaystyle B}$${\displaystyle A}$${\displaystyle a:A}$${\displaystyle B(a)}$${\displaystyle a}$${\displaystyle \exists {a}{\in }A\,B(a)}$${\textstyle \sum _{a:A}B(a)}$

たとえば、が より小さいか等しいのは、 となる別の自然数が存在する場合のみです。論理学では、このステートメントは存在量化によってコード化されます。 ${\displaystyle m:\mathbb {N} }$${\displaystyle n:\mathbb {N} }$${\displaystyle k:\mathbb {N} }$${\displaystyle m+k=n}$

$${\displaystyle m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.}$$

この命題は従属ペア型に対応します:

$${\displaystyle \sum _{k:\mathbb {N} }m+k=n.}$$

つまり、 がより小さいか等しいという命題の証明は、との差である負でない数と、等式 の証明の両方を含むペアです。 ${\displaystyle m}$${\displaystyle n}$${\displaystyle k}$${\displaystyle m}$${\displaystyle n}$${\displaystyle m+k=n}$

Henk Barendregt は、3 つの軸に沿って型システムを分類する手段としてラムダ キューブを開発しました。結果として得られる立方体の形をした図の 8 つの角はそれぞれ型システムに対応しており、最も表現力の低い角には単純型ラムダ計算、最も表現力の高い角には構成の計算が配置されています。立方体の 3 つの軸は、単純型ラムダ計算の 3 つの異なる拡張、つまり依存型の追加、ポリモーフィズムの追加、およびより高次の型コンストラクタ (たとえば、型から型への関数) の追加に対応しています。ラムダ キューブは、純粋型システムによってさらに一般化されています。

論理フレームワークLFに対応する純粋な一階従属型のシステムは、単純型ラムダ計算の関数空間型を従属積型に一般化することによって得られます。 ${\displaystyle \lambda \Pi }$

2 次従属型のシステムは、型コンストラクタの量化を許可することで から得られます。この理論では、従属積演算子は、単純型付きラムダ計算の演算子とSystem Fのバインダーの両方を包含します。 ${\displaystyle \lambda \Pi 2}$${\displaystyle \lambda \Pi }$${\displaystyle \to}$${\displaystyle \forall}$

高階システムは、ラムダ キューブからの 4 つの抽象化形式すべてに拡張されます。つまり、項から項、型から型、項から型、型から項への関数です。このシステムは、その導関数である帰納的構成の計算がCoq 証明支援システムの基礎となるシステムである構成の計算に対応しています。 ${\displaystyle \lambda \Pi \omega }$${\displaystyle \lambda \Pi 2}$

カリー・ハワード対応は、任意の複雑な数学的特性を表現する型を構築できることを意味します。ユーザーが、型が存在する（つまり、その型の値が存在する）という構成的証明を提供できれば、コンパイラはその証明をチェックし、構築を実行して値を計算する実行可能なコンピュータ コードに変換できます。証明チェック機能により、依存型言語は証明支援機能と密接に関連しています。コード生成の側面は、機械的に検証された数学的証明から直接コードが派生するため、 正式なプログラム検証と証明付きコードへの強力なアプローチを提供します。

• 型付きラムダ計算
• 直観主義型理論

• 依存型プログラミング 2008
• 依存型プログラミング 2010
• 依存型プログラミング 2011
• Haskell Wiki の「依存型」
• nラボにおける依存型理論
• nラボの依存型
• nラボの依存製品タイプ
• nラボでの従属和型
• nラボの依存製品
• nラボの従属合計