|
計算機科学と論理学において、依存型とは値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義的型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS (プログラミング言語)、Agda、Idris、Epigramなどのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。 依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の''値''に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるというポリモーフィズムとは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。 依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は型検査は決定不能となってしまう。 ==歴史== 依存型は、プログラミングと論理学のつながりを深めるために作られた。 1934年にハスケル・カリーは、当時考えられていた数学的なプログラミング言語で使われていた型が、命題論理の公理系と同じパターンに従っていることを発見した。さらに、命題論理の証明それぞれに対して、プログラミング言語における関数(項)が対応していることもわかった。カリーの挙げた例の一つは、単純型付きラムダ計算と直観主義論理の対応である。 述語論理は命題論理に量化子を加えたものである。ハワードとド・ブラウンは型付きラムダ計算に依存関数のための型("任意の"に対応する)と依存ペアのための型("存在する"に対応する)を加えることで、述語論理に対応するプログラミング言語を作り出した。 (これを含むいくつかの業績により、命題を型と見なす考え方はカリー＝ハワード同型対応という名前で知られている。) 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「依存型」の詳細全文を読む スポンサード リンク
|