Teoria dei tipi

Dal punto di vista più generale, la teoria dei tipi è la branca della matematica e della logica che si occupa di classificare generiche entità, raggruppandole in collezioni chiamate tipi. Sotto questo punto di vista vi sono punti di contatto con la nozione di tipo della metafisica. La moderna formulazione della teoria dei tipi è, in parte, nata dal tentativo di dare una risposta al cosiddetto Paradosso di Russell, ed è estesamente trattata nei Principia Mathematica di Bertrand Russell e Alfred North Whitehead.

Con la diffusione di computer sempre più potenti, e l'introduzione di linguaggi di programmazione per lo sviluppo di programmi, la teoria dei tipi ha trovato un significativo campo di applicazione, soprattutto nell'ambito della progettazione degli stessi linguaggi di programmazione. In questo contesto, esistono diverse definizioni applicabili a un sistema dei tipi, ma la seguente, dovuta a Benjamin C. Pierce è probabilmente quella che raccoglie il maggiore consenso:

"Un sistema di tipi è un metodo sintattico trattabile, in grado di dimostrare l'assenza di determinati comportamenti nei programmi mediante la classificazione di espressioni fatta in base alla natura dei valori che esse elaborano."

(Types and Programming Languages, MIT Press, 2002)

In altre parole, un sistema di tipi divide i valori manipolati dai programmi in insiemi chiamati tipi - eseguendo un'operazione chiamata assegnazione del tipo o tipizzazione - e fa sì che certi determinati comportamenti del programma siano, o non siano, possibili in base al tipo dei valori coinvolti in questi comportamenti.

Per esempio, supponiamo che un sistema di tipi classifichi il valore ciao come stringa e il valore 5 come intero e, sulla base di tali diverse assegnazioni, proibisca al programmatore di sommare ciao a 5. All'interno di questo sistema, sarebbe "illegale" l'istruzione di programma:

ciao + 5

Il vantaggio di questa "proibizione", ovvero dell'impossibilità di far eseguire al programma questa operazione, consiste nel fatto che non potrà mai capitare di sommare stringhe a numeri, operazione che produrrebbe risultati privi di senso.

La progettazione e l'implementazione di un sistema di tipi è un argomento vasto e complesso, quasi come lo stesso linguaggio di programmazione che lo utilizza. Gli ideatori e gli studiosi dei sistemi di tipi si spingono ad affermare che si tratta dell'essenza stessa del linguaggio:

«Progettate correttamente il sistema dei tipi e vedrete che il linguaggio si progetterà da sé!^{[senza fonte]}»

È importante notare che la trattazione fin qui fatta si riferisce ai tipi statici. I sistemi di tipi ed i linguaggi che fanno uso di tipi dinamici non sono in grado di verificare a priori che un programma faccia un uso corretto dei valori, e quindi generano un errore ogni volta che il programma si comporta in modo da farne un uso scorretto. Per questa ragione, secondo alcuni^{[senza fonte]}, la definizione "tipo dinamico" è intrinsecamente poco appropriata. Comunque, in molti linguaggi orientati agli oggetti che fanno uso di tipi dinamici, un tipo è qualcosa di più di un'interfaccia e, finché le classi condividono interfacce, non è necessario preoccuparsi di sapere a quale classe appartiene un dato oggetto.