依存型

依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS、Agda、Idris、Epigramなどのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。

依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。

依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は型検査は決定不能となってしまう。

歴史

依存型は、プログラミングと論理学のつながりを深めるために作られた。

1934年にハスケル・カリーは、当時考えられていた数学的なプログラミング言語で使われていた型が、命題論理の公理系と同じパターンに従っていることを発見した。さらに、命題論理の証明それぞれに対して、プログラミング言語における関数(項)が対応していることもわかった。カリーの挙げた例の一つは、単純型付きラムダ計算と直観主義論理の対応である。

述語論理は命題論理に量化子を加えたものである。ハワードとド・ブラウンは型付きラムダ計算に依存関数のための型("任意の"に対応する)と依存ペアのための型("存在する"に対応する)を加えることで、述語論理に対応するプログラミング言語を作り出した。

(これを含むいくつかの業績により、命題を型と見なす考え方はカリー＝ハワード同型対応という名前で知られている。)

形式的な定義

非常に大雑把に説明すると、依存型は添字づけられた集合の族によって与えられると考えることができる。より形式的には、$A:{\mathcal {U}}$を${\mathcal {U}}$(型のなす宇宙)に属する型としたときに、型のなす族$B:A\to {\mathcal {U}}$を考えることができる。すなわち、$A$に属する値$a:A$それぞれについて、型$B(a):{\mathcal {U}}$が割り当てられているのである。終域が引数に応じて変化する関数は依存関数と呼ばれ、このような関数のための型は依存型、依存積型、あるいはΠ型と呼ばれる。この例では、依存積型は

$\Pi _{(x:A)}B(x)$

あるいは

$\Pi (x:A),B(x)$

と表記される。

もしBが定数関数$B(x)=C$であるなら、依存積型は通常の関数型(矢印型)$A\to C$となる。つまり、$\Pi _{(x:A)}B$は型判定において関数型$A\to C$と等しい。

Π型という名前は、依存積型が型の直積と見なせるという考え方に由来している。依存積型は全称量化のモデルとして理解することもできる。

例えば、実数の$n$個の対を${\mbox{Vec}}({\mathbb {R} },n)$と表記するとき、$\Pi _{(n:{\mathbb {N} })}{\mbox{Vec}}({\mathbb {R} },n)$は、自然数nを受け取りn個の実数の対を返す関数の型である。通常の関数空間は、依存積型で戻り値の型が実際には引数に依存しない特別な場合としてあらわれる。例えば、$\Pi _{(n:{\mathbb {N} })}\;{\mathbb {R} }$は自然数から実数への関数の型であり、単純型付きラムダ計算では${\mathbb {N} }\to {\mathbb {R} }$と表記される。

型多相な関数は依存関数(すなわち、依存積型をもつ関数)の重要な例である。多相関数は、型を与えられると、その型を含む型を持つ値として振る舞う。例えば、恒等関数、すなわち任意の型Aに対し$a:A$を受け取りaをそのまま返す関数、の型は、

$\Pi _{(A:{\mathcal {U}})}A\to A$

と書くことができる。

依存ペア型

依存積型の双対は、依存ペア型、依存和型、あるいはΣ型と呼ばれる型である。これは余積や直和、非交和などのアナロジーである。依存和型は存在量化のモデルとして理解することもできる。依存和型は

$\Sigma _{(x:A)}B(x)$

と表記される。

依存和型は、2番目の型が1番目の値に応じて変化するペアの型を表している。したがって、もし

$(a,b):\Sigma _{(x:A)}B(x)$

ならば、$a:A$であり、$b:B(a)$である。Bが定数関数$B(x)=C$のときは、依存和型は直積型、すなわち通常の直積$A\times C$と一致する(型判定において一致する)。

存在量化としての例

$\Sigma AB_{a}:{\mathcal {U}}$を、型$A:{\mathcal {U}}$上で述語$B:A\rightarrow {\mathcal {U}}$を量化した依存和型とする。このとき、$B_{a}$が成立する$a:A$が存在することと、$\Sigma AB_{a}$が非空であることが同値である。例えば、aがb以下であることと、自然数nとa+n=bの証明の組が存在することが同値である。

$a\leq b\iff \Sigma \mathbb {N} (\lambda n\rightarrow a+n=b)$

ラムダ・キューブ

ヘンク・バレンドレクト (en:Henk Barendregt) はいくつかの型システムを3つの軸にそって分類するラムダ・キューブを発明した。立方体の形をした図の8個の頂点それぞれが型システムに対応している。単純型付きラムダ計算が最も表現力が低い頂点に配置され、Calculus of constructions (en:Calculus of constructions)が最も表現力が高い頂点に配置されている。立方体の3個の軸はそれぞれ単純型付きラムダ計算に対する3種類の異なる拡張を意味している。それぞれ、依存型の追加、型多相性の追加、高階のカインド (en:Kind (type theory)) を持つ型コンストラクタ (例えば型から型への関数) の追加、である。ラムダ・キューブは純粋型システム (en:Pure type system)によってさらに一般化される。

ラムダ・キューブにおける(狭義の)依存型と多相型は、どちらも(広義の)依存積型の特別な場合と見なせるが、値に関する量化をする場合は(狭義の)依存型、型や型コンストラクタに関する量化をする場合は多相型と呼び、区別される。ラムダ・キューブにおけるカインド(通常の型を集めた特別な型)を$*$, 超カインド(カインドを集めた特別な型)を$\square$と表記する。このとき、(狭義の)依存型とは、$A:*$および$B:A\to *$を用いて構成される、$\Pi _{(x:A)}B(x)$という型のことである。一方、多相型は、$A:\square$および$B:A\to *$を用いて構成される、$\Pi _{(x:A)}B(x)$という型のことである。例えば、$*:\square$であることを用いて$\Pi _{(x:*)}B(x)$と書いたものは、型に関する量化をしている多相型となる。

一階の依存型理論

一階の依存型を持つ$\lambda \Pi$型システムは、単純型付きラムダ計算の関数型(矢印型)を依存積型に一般化することで得られる。これは論理学におけるLogical Framework LF (en:Logical framework#LF)に対応する。

二階の依存型理論

二階の依存型を持つ$\lambda \Pi 2$型システムは、$\lambda \Pi$に型コンストラクタ上での量化を許容することで得られる。この型システムでは、依存積演算子は単純型付きラムダ計算の$\to$演算子とSystem Fの$\forall$束縛子の両方の役割を果たす。

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

高階の$\lambda \Pi \omega$型システムは$\lambda \Pi 2$を、ラムダ・キューブの4つ全てのラムダ抽象の形式に拡張することで得られる。すなわち、項から項への関数、型から項への関数、項から型への関数、そして型から型への関数である。この型システムはCalculus of constructionsに対応する。Calculus of constructionsをさらに拡張するとCalculus of inductive constructions (en:Calculus of inductive constructions) が得られる。これは、Coqが用いている型システムである。

プログラミング言語と論理学の両立

カリー＝ハワード同型対応により、どんなに複雑な数学的な性質も型によって表現できる。もしユーザーが、型が非空である (つまり、その型を持つ値が存在する) ことの構成的な証明を与えることができれば、コンパイラは証明の正当性を検査し、証明の構成を追うことにより、実際にその値を計算できる実行可能なプログラムコードを出力することができる。このように証明を検査できるという性質により、依存型を持つプログラミング言語は定理証明支援系と近い関係にある。コードを生成できるという視点からは、機械的に検証された数学の証明からプログラムコードを直接導出することができるため、形式手法によるプログラム検証や証明つきコードへのアプローチが考えられる。

関連項目

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