In computer science and logic, a dependent type is a type that depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like ATS, Agda, Idris and Epigram, dependent types prevent bugs by allowing extremely expressive types.Two common examples of dependent types are dependent functions and dependent pairs.