依存型
非常に大雑把に説明すると、依存型は添字づけられた集合の族によって与えられると考えることができる。より形式的には、 A : U {\displaystyle A:{\mathcal {U}}} を U {\displaystyle {\mathcal {U}}} (型のなす宇宙)に属する型としたときに、型のなす族 B : A → U {\displaystyle B:A\to {\mathcal {U}}} を考えることができる。すなわち、 A {\displaystyle A} に属する値 a : A {\displaystyle a:A} それぞれについて、型 B ( a ) : U {\displaystyle B(a):{\mathcal {U}}} が割り当てられているのである。終域が引数に応じて変化する関数は依存関数と呼ばれ、このような関数のための型は依存型、依存積型、あるいはΠ型と呼ばれる。この例では、依存積型は
Π ( x : A ) B ( x ) {\displaystyle \Pi _{(x:A)}B(x)}
あるいは
Π ( x : A ) , B ( x ) {\displaystyle \Pi (x:A),B(x)}
と表記される。
もしBが定数関数 B ( x ) = C {\displaystyle B(x)=C} であるなら、依存積型は通常の関数型(矢印型) A → C {\displaystyle A\to C} となる。つまり、 Π ( x : A ) B {\displaystyle \Pi _{(x:A)}B} は型判定において関数型 A → C {\displaystyle A\to C} と等しい。
依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS(英語版)、Agda、Idris(英語版)、Epigram(英語版)などのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。
依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。
依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は型検査は決定不能となってしまう。