La Teoria dei Tipi fu sviluppata da Bertrand Russell (principalmente nei Principia Mathematica, scritti con Alfred North Whitehead) come soluzione diretta al paradosso che portava il suo nome. L’obiettivo di Russell era “sanare” la logica e la teoria degli insiemi, impedendo la formazione di quegli insiemi auto-referenziali che generavano contraddizioni (come l’insieme di tutti gli insiemi che non appartengono a se stessi).

Il concetto cardine della teoria è che gli oggetti logici non sono tutti sullo stesso piano, ma appartengono a livelli o “tipi” differenti (gerarchie differenti). Una proprietà (o un insieme) appartiene sempre a un tipo superiore rispetto agli oggetti a cui si applica. Russell stabilì una regola ferrea: una funzione proposizionale non può mai avere come argomento se stessa, né può far parte del proprio dominio. Vediamo la gerarchia dei tipi (semplificata):

• Tipo 0: gli individui (oggetti fisici, numeri singoli, entità che non sono insiemi).
• Tipo 1: proprietà di individui o insiemi di individui (es: “l’insieme dei numeri pari”).
• Tipo 2: proprietà di proprietà o insiemi di insiemi (es: “l’insieme delle classi infinite”).
• Tipo n+1: oggetti che hanno come elementi entità di tipo n.

Riprendendo il paradosso del barbiere che rade “tutti coloro che non si radono da soli”, la Teoria dei Tipi interviene dicendo che il “barbiere” (l’operatore/insieme) è di un tipo logico superiore rispetto agli “uomini del villaggio” (gli elementi). Di conseguenza, la regola che definisce chi deve essere rasato dal barbiere non può applicarsi al barbiere stesso, perché lui non appartiene al tipo logico degli oggetti su cui opera. In questo modo, la domanda “il barbiere si rade da solo?” diventa logicamente priva di senso (una non-sense sentence), poiché viola la gerarchia dei tipi.

Russell dovette rendere la teoria più complessa per evitare altre forme di paradossi (quelli semantici, come il paradosso del mentitore) come segue:

• Teoria semplice dei tipi: si limita a distinguere tra individui, classi, classi di classi, ecc. Risolve i paradossi logico-matematici;
• Teoria ramificata dei tipi: introduce il concetto di “ordine”. Anche all’interno dello stesso tipo, le definizioni che fanno riferimento a una totalità appartengono a un ordine superiore. Questo serviva a evitare la “circolarità viziosa” nelle definizioni.

La teoria ramificata era così rigida da rischiare di paralizzare la matematica (rendendo difficili definizioni comuni come quelle dei numeri reali). Per ovviare a questo, Russell dovette introdurre l’Assioma di Riducibilità, che permetteva di “abbassare” una proprietà di ordine superiore a un ordine inferiore (proprietà predicativa). Questo assioma fu molto criticato perché appariva come una soluzione “ad hoc”, meno elegante e meno puramente logica del resto del sistema.

La Teoria dei Tipi di Russell è l’antenata diretta dei sistemi di tipi nei linguaggi di programmazione. Quando un compilatore ti dà un errore perché stai cercando di sommare una “stringa” a un “numero intero”, sta applicando una versione moderna della gerarchia di Russell. I linguaggi funzionali avanzati (come Haskell o Agda) si basano su evoluzioni di questa teoria (come la Teoria dei Tipi di Martin-Löf).