Dependent type

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Rocq (previously known as Coq), F*, Epigram, Idris, and Lean, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

Two common examples of dependent types are dependent functions and dependent pairs. The return type of a dependent function may depend on the value (not just type) of one of its arguments. For instance, a function that takes a positive integer $n$ may return an array of length $n$ , where the array length is part of the type of the array. (Note that this is different from polymorphism and generic programming, both of which include the type as an argument.) A dependent pair may have a second value, the type of which depends on the first value. Sticking with the array example, a dependent pair may be used to pair an array with its length in a type-safe way.

Dependent types add complexity to a type system. Deciding the equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence the decidability of type checking may depend on the given type theory's semantics of equality, that is, whether the type theory is intensional or extensional.^[1]

History

In 1934, Haskell Curry noticed that the types used in typed lambda calculus, and in its combinatory logic counterpart, followed the same pattern as axioms in propositional logic. Going further, for every proof in the logic, there was a matching function (term) in the programming language. One of Curry's examples was the correspondence between simply typed lambda calculus and intuitionistic logic.^[2]

述語論理は命題論理の拡張であり、量化子を追加したものです。ハワードとデ・ブルインは、このより強力な論理に合わせてラムダ計算を拡張し、「すべて」に対応する依存関数と、「存在する」に対応する依存ペアの型を作成しました。^{[ 3 ]}

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

正式な定義

依存型理論において、依存型とは、値によって仕様が変化する可能性のある型であり、インデックス付き集合族に類似するものと見なすことができる。 ${\mathcal {U}}$ 型の集合を表し、 $A:{\mathcal {U}}$ 示すために $A$ はタイプです ${\mathcal {U}}$ 期間 $a$ タイプの $A$ 、書く $a:A$ 型の依存ファミリー $A$ 書かれている $B:A\to {\mathcal {U}}$ つまり、各項に対して $a:A$ 家族はタイプを割り当てます $B(a):{\mathcal {U}}$ したがって、 $A:{\mathcal {U}}$ そして $B:A\to {\mathcal {U}}$ 表現 $B(a)$ 特定の値に依存する型を示します $a$ 標準的な用語では、これは次のように表現されます。 $B(a)$ 異なる $a$ 。

Π型

戻り値の型が引数によって変化する関数（つまり、固定された終域を持たない関数）は従属関数であり、この関数の型は従属積型、π型（ $Π$ 型）、または従属関数型と呼ばれる。^{[ 4 ]}型のファミリーから $B:A\to {\mathcal {U}}$ 依存関数のタイプを構築することができます ${\textstyle \prod _{x:A}B(x)}$ 項は、項を取る関数である。 $a:A$ そして、次の項を返します。 $B(a)$ この例では、依存関数型は通常次のように記述されます。 ${\textstyle \prod _{x:A}B(x)}$ または ${\textstyle \prod {(x:A)}B(x)}$ 。

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

「Π型」という名称は、これらが型のデカルト積として捉えられるという考え方に由来する。Π型は、全称量化子のモデルとしても理解できる。

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

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

Σ型

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

依存ペア型は、2 番目の項の型が最初の項の値に依存する順序対の概念を捉えています。 ${\textstyle (a,b):\sum _{x:A}B(x),}$ それから $a:A$ そして $b:B(a)$ 。もし $B$ が定数関数である場合、従属ペアのタイプは積のタイプ、つまり通常のデカルト積になります（判断上等になります）。 $A\times B$ [ ⁴^]

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

存在量化の例

させて $A:{\mathcal {U}}$ あるタイプとし、 $B:A\to {\mathcal {U}}$ カリーとハワードの書簡によると、 $B$ は、以下の用語に関する論理述語として解釈できる。 $A$ 特定の $a:A$ 種類が $B(a)$ 居住されているかどうかは、 $a$ この述語を満たす。この対応関係は存在量化と依存ペアに拡張できる。命題 $\exists {a}{\in }A\,B(a)$ 型が真である場合に限り真となります。 ${\textstyle \sum _{a:A}B(a)}$ 人が住んでいる。

例えば、 $m:\mathbb {N}$ 以下 $n:\mathbb {N}$ 別の自然数が存在する場合に限る $k:\mathbb {N}$ そのため $m+k=n$ 論理学において、この命題は存在量化によって体系化される。

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

この命題は、従属対タイプに対応します。

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

つまり、次の主張の証明 $m$ 以下 $n$ 非負の数を含むペア $k$ これは、 $m$ そして $n$ 等号の証明 $m+k=n$ 。

ラムダキューブのシステム

ヘンク・バレンデレヒトは、型システムを3つの軸に沿って分類する手段としてラムダキューブを開発しました。結果として得られる立方体状の図の8つの角はそれぞれ型システムに対応しており、最も表現力の低い角には単純型ラムダ計算が、最も表現力の高い角には構成計算が配置されています。立方体の3つの軸は、単純型ラムダ計算の3つの異なる拡張に対応しています。すなわち、依存型の追加、多相性の追加、およびより高次の型コンストラクタ（例えば、型から型への関数）の追加です。ラムダキューブは、純粋型システムによってさらに一般化されます。

一次依存型理論

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

二次依存型理論

システム $\lambda \Pi 2$ 2次依存型のものは以下から得られる。 $\lambda \Pi$ 型コンストラクタに対する量化を可能にすることによって。この理論では、依存積演算子は、 $\to$ 単純型ラムダ計算の演算子と $\forall$ システムFのバインダー。

高階依存型多相ラムダ計算

高次システム $\lambda \Pi \omega$ 拡張 $\lambda \Pi 2$ ラムダキューブからの4つの抽象化形式すべてに対応します。すなわち、項から項、型から型、項から型、型から項への関数です。このシステムは構成計算に対応し、その導関数である帰納的構成計算はRocqの基盤となるシステムです。

同時プログラミング言語とロジック

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

従属型を持つ言語の比較

↑これはコア言語を指しており、タクティクス（定理証明手続き）やコード生成サブ言語を指しているわけではありません。
↑意味論的制約（宇宙制約など）に従う
↑リングソルバー^{[ 6 ]}
↑オプションのユニバース、オプションのユニバース多相性、およびオプションの明示的に指定されたユニバース
↑ユニバース、自動的に推論されるユニバース制約（Agdaのユニバース多相性とは異なる）、およびオプションの明示的なユニバース制約の出力
↑ ATSに置き換えられました
↑ Sageの最新論文と最新のコードスナップショットはどちらも2006年のものです

参考文献

↑ホフマン、マーティン (1995)、内包型理論における外延概念(PDF)
↑ Sørensen, Morten Heine B.; Urzyczyn, Pawel (1998), Lectures on the Curry-Howard Isomorphism , CiteSeerX 10.1.1.17.7385
↑ Bove, Ana; Dybjer, Peter (2008).職場における依存型(PDF) (レポート). チャルマース工科大学。
1 2 3 Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas (2010). "ΠΣ: 糖衣のない依存型" (PDF) . In Blume, Matthias; Kobayashi, Naoki; Vidal, Germán (eds.). Functional and Logic Programming, 10th International Symposium, FLOPS 2010, 仙台, 日本, 2010年4月19-21日. Proceedings . Lecture Notes in Computer Science. Vol. 6009. Springer. pp. 40– 55. doi : 10.1007/978-3-642-12251-4_5 .
↑ 「Agdaダウンロードページ」
↑ 「Agda Ring Solver」。
1 2 "アナウンス: Agda 2.2.8"。2011年7月18日にオリジナルからアーカイブされました。2010年9月28日に取得。
↑ "Agda 2.6.0 変更履歴"。
↑ 「ATS2 ダウンロード」
↑ 「ATSの発明者であるホンウェイ・シーからのメール」。
↑ Xi, Hongwei (2017年3月). "応用型システム: 定理証明による実践的プログラミングへのアプローチ" (PDF) . arXiv : 1703.08683 .
↑ 「SubversionリポジトリにおけるCoqの変更」。
↑ 「Coq 8.10 における SProp の導入」。
↑ "GitHub での変更点" . GitHub .
↑ "F* v0.9.5.0 リリースノート on GitHub" . GitHub .
↑ 「Guru SVN」。
1 2アーロン・スタンプ (2009 年 4 月 6 日)。「Guru での検証済みプログラミング」(PDF)。2009年 12 月 29 日にオリジナル(PDF)からアーカイブ済み。2010年9 月 28 日に取得。
↑ペッチャー、アダム（2008年5月）。操作型理論における基底方程式による結合可能性の決定（PDF）（修士論文）。ワシントン大学。 2010年10月14日取得。
↑ "Idris git repository" . GitHub . 2022年5月17日。
↑ Brady, Edwin. "Idris、依存型を持つ言語 — 拡張要約" (PDF) . CiteSeerX 10.1.1.150.9442 .
↑ 「Matita SVN」。2006年5月8日にオリジナルからアーカイブ済み。2010年9月29日に取得。

さらに読む

Martin-Löf, Per (1984).直観主義型理論(PDF) . Bibliopolis.
ノードストローム、ベングト。ケント州ピーターソン。スミス、ヤン・M. (1990)。Martin-Löf の型理論におけるプログラミング: 入門。オックスフォード大学出版局。ISBN 9780198538141。
Barendregt, H. (1992). "型付きラムダ計算" . Abramsky, S.、Gabbay, D.、Maibaum, T. (編) 『コンピュータサイエンスにおける論理ハンドブック』所収。Oxford Science Publications。doi : 10.1017/CBO9781139032636 . hdl : 2066/17231。
ブランドル、ヘルムート（2022）。構成の計算
McBride, Conor ; McKinna, James (2004 年 1 月). 「左からの視点」 . Journal of Functional Programming . 14 (1): 69–111 . doi : 10.1017/s0956796803004829 . S2CID 6232997 .
Altenkirch, Thorsten ; McBride, Conor ; McKinna, James (2006). 「依存型が重要な理由」（PDF） .第33回ACM SIGPLAN-SIGACTプログラミング言語原理シンポジウム（POPL 2006）議事録、米国サウスカロライナ州チャールストン、1月11日～13日. ISBN 1-59593-027-2。
Norell, Ulf (2007年9月).依存型理論に基づく実用的なプログラミング言語に向けて(PDF) (博士論文). スウェーデン、ヨーテボリ: チャルマース工科大学コンピュータ科学・工学部. ISBN 978-91-7291-996-9。
Oury, Nicolas; Swierstra, Wouter (2008). "The Power of Pi" (PDF) . ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming . pp. 39–50 . doi : 10.1145/1411204.1411213 . ISBN 9781595939197. S2CID 16176901 .
ノレル、ウルフ (2009)。「Agda での依存型プログラミング」(PDF)。コープマン、P.プラスマイヤー、R.スウィアストラ、D. (編)。高度な関数型プログラミング。 2008 年 AFP。コンピューターサイエンスの講義ノート。 Vol. 5832.スプリンガー。 pp. 230–266 .土井: 10.1007/978-3-642-04652-0_5。ISBN 978-3-642-04651-3。
シトニコフスキー、ボロ（2018）。『イドリスによる依存型入門』リーン・パブリッシング。ISBN 978-1723139413。
McBride, Conor ; Nordvall-Forsberg, Fredrik (2022). 「次元を考慮したプログラムのための型システム」(PDF) . Advanced Mathematical and Computational Tools in Metrology and Testing XII . Advances in Mathematics for Applied Sciences. World Scientific. pp. 331–345 . doi : 10.1142/9789811242380_0020 . ISBN 9789811242380. S2CID 243831207 .

外部リンク

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

[5] これはコア言語を指しており、タクティクス（定理証明手続き）やコード生成サブ言語を指しているわけではありません。

[6] 意味論的制約（宇宙制約など）に従う

[9] リングソルバー^{[ 6 ]}

[10] オプションのユニバース、オプションのユニバース多相性、およびオプションの明示的に指定されたユニバース

[17] ユニバース、自動的に推論されるユニバース制約（Agdaのユニバース多相性とは異なる）、およびオプションの明示的なユニバース制約の出力

[19] ATSに置き換えられました

[28] Sageの最新論文と最新のコードスナップショットはどちらも2006年のものです

[extensional-1] ホフマン、マーティン (1995)、内包型理論における外延概念(PDF)

[curry_howard-2] Sørensen, Morten Heine B.; Urzyczyn, Pawel (1998), Lectures on the Curry-Howard Isomorphism , CiteSeerX 10.1.1.17.7385

[dep_types_at_work-3] Bove, Ana; Dybjer, Peter (2008).職場における依存型(PDF) (レポート). チャルマース工科大学。

[without-sugar-4] 1 2 3 Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas (2010). "ΠΣ: 糖衣のない依存型" (PDF) . In Blume, Matthias; Kobayashi, Naoki; Vidal, Germán (eds.). Functional and Logic Programming, 10th International Symposium, FLOPS 2010, 仙台, 日本, 2010年4月19-21日. Proceedings . Lecture Notes in Computer Science. Vol. 6009. Springer. pp. 40– 55. doi : 10.1007/978-3-642-12251-4_5 .

[7] 「Agdaダウンロードページ」

[8] 「Agda Ring Solver」。

[agda-2.2.8-11] 1 2 "アナウンス: Agda 2.2.8"。2011年7月18日にオリジナルからアーカイブされました。2010年9月28日に取得。

[12] "Agda 2.6.0 変更履歴"。

[13] 「ATS2 ダウンロード」

[14] 「ATSの発明者であるホンウェイ・シーからのメール」。

[15] Xi, Hongwei (2017年3月). "応用型システム: 定理証明による実践的プログラミングへのアプローチ" (PDF) . arXiv : 1703.08683 .

[16] 「SubversionリポジトリにおけるCoqの変更」。

[18] 「Coq 8.10 における SProp の導入」。

[20] "GitHub での変更点" . GitHub .

[21] "F* v0.9.5.0 リリースノート on GitHub" . GitHub .

[22] 「Guru SVN」。

[guru-book-23] 1 2アーロン・スタンプ (2009 年 4 月 6 日)。「Guru での検証済みプログラミング」(PDF)。2009年 12 月 29 日にオリジナル(PDF)からアーカイブ済み。2010年9 月 28 日に取得。

[hypjoin-paper-24] ペッチャー、アダム（2008年5月）。操作型理論における基底方程式による結合可能性の決定（PDF）（修士論文）。ワシントン大学。 2010年10月14日取得。

[25] "Idris git repository" . GitHub . 2022年5月17日。

[26] Brady, Edwin. "Idris、依存型を持つ言語 — 拡張要約" (PDF) . CiteSeerX 10.1.1.150.9442 .

[27] 「Matita SVN」。2006年5月8日にオリジナルからアーカイブ済み。2010年9月29日に取得。

[1]

[2]

[ 3 ]

[ 4 ]

[ 6 ]

Dependent type

History

正式な定義

Π型

Σ型

存在量化の例

ラムダキューブのシステム

一次依存型理論

二次依存型理論

高階依存型多相ラムダ計算

同時プログラミング言語とロジック

従属型を持つ言語の比較

関連項目

参考文献

さらに読む

外部リンク

関連するトピック

computer science

logic

type theory

type systems