CentralNotice Dependent type From Wikipedia, the free encyclopedia Jump to: navigation , search Type systems Type safety Dynamic type-checking Static type-checking Inferred vs. Manifest Nominal vs. Structural Dependent typing Duck typing Latent typing Substructural typing Uniqueness typing Strong and weak typing v t e In computer science and logic , a dependent type is a type that depends on a value. It is an overlapping feature of math-encoding type theory and bug-stopping 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 very expressive types. Two common examples of dependent types are dependent functions and dependent pairs. A dependent function's retur...