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 (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une...) 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 (Le lambda-calcul (ou λ-calcul) est un langage de programmation théorique inventé par Alonzo Church dans les années 1930. Ce langage a été le premier utilisé pour définir et caractériser les fonctions...).
En théorie des types (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.), les entités mathématiques (Les mathématiques constituent un domaine de connaissances abstraites construites à l'aide de raisonnements logiques sur des concepts tels que les nombres, les figures, les structures et les transformations....) 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 :