依存型

依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。、Agda、、などのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。 依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の値に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。 依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合ははとなってしまう。