Залежны тып () у інфарматыцы і логіцы — тып, які залежыць ад некаторага значэння. Залежныя тыпы граюць ключавую ролю ў інтуіцыянісцкай тэорыі тыпаў і пабудове функцыянальных моў праграмавання такіх як ATS, Agda, і Idris .
Напрыклад, тып, які апісвае n — картэжы сапраўдных лікаў, з’яўляецца залежным, бо ён «залежыць» ад велічыні n.
Рашэнне аб роўнасці залежных тыпаў у праграме можа запатрабаваць вылічэнняў. Калі ў залежных тыпах дапушчана выкарыстанне адвольных значэнняў, то рашэнне аб роўнасці тыпаў можа складацца з праверкі роўнасці выніку працы дзвюх адвольных праграм. Такім чынам, праверка тыпу становіцца невырашальнай задачай.
Ізамарфізм Кары — Ховарда дазваляе будаваць тыпы для выражэння колькі заўгодна складаных матэматычных уласцівасцяў. Калі прадстаўлены канструктыўны доказ таго, што тып «заселены» (гэта значыць, існуе хаця б адно значэнне гэтага тыпу), кампілятар зможа праверыць гэты доказ і ператварыць яго ў выкананы код, які вылічае значэнне. Наяўнасць праверкі доказаў робіць залежна-тыпізаваныя мовы падобнымі да праграмнага забеспячэння аўтаматызацыі доказаў (напрыклад, інтэрактыўны доказ тэарэм Coq).
Катэгорыя:Тыпы даных