依存型
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/29 03:08 UTC 版)
依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS、Agda、Idris、Epigramなどのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。
- ^ Sørensen, Morten Heine B.; Pawel Urzyczyn (1998). Lectures on the Curry-Howard Isomorphism .
- ^ Bove, Ana; Peter Dybjer (2008). Dependent Types at Work .
- ^ Peterka, Ondrej (2007). Dependent Types In Lambda Cube .
- 依存型のページへのリンク