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 connaissance spéculative, souvent basée sur l’observation ou...) 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...) 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 :

• la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans une première approche l'étude...) pour laquelle on cherche à donner un contenu calculatoire aux propositions et aux démonstrations par la correspondance (La correspondance est un échange de courrier généralement prolongé sur une longue période. Le terme désigne des échanges de courrier personnels plutôt qu'administratifs.) de Curry Howard,
• les langages de programmation (La programmation dans le domaine informatique est l'ensemble des activités qui permettent l'écriture des programmes informatiques. C'est une étape importante de la conception de logiciel (voire de matériel, cf. VHDL).), surtout les langages fonctionnels typés,
• les systèmes de démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de...) sur ordinateur (Un ordinateur est une machine dotée d'une unité de traitement lui permettant d'exécuter des programmes enregistrés. C'est un ensemble de circuits électroniques...).