La théorie des types est une branche de la logique mathématique : elle fonde la construction des objets sur la notion de fonction et non pas sur celle d'ensemble.
Une première théorie des types a été créée par Bertrand Russell pour résoudre les paradoxes de la théorie des ensembles ; lourde d'emploi, elle a été supplantée par la théorie de Zermelo-Frankel avant d'être réconsidérée après la découverte du lambda-calcul.
En théorie des types, les entités mathématiques sont construites à l'aide de fonctions, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les entités sont bien formées lorsque les fonctions sont appliquées à des entités ayant le type que la fonction attend.
Le concept de type a plusieurs domaines d'applications :