Teoria dei tipi

Da Wikipedia, l'enciclopedia libera.

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 Russell e Whitehead.

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

"Un sistema di tipi è un metodo sintattico modificabile, in grado di dimostrare l'assenza di determinati comportamenti nei programmi mediante la classificazione di espressioni fatta in base alla natura dei valori sottoposti ad elaborazione."

(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 ed 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, l'istruzione di programma:

ciao + 5

sarebbe illegale. 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 effermare che si tratta dell'essenza stessa del linguaggio:

"Progettate correttamente il sistema dei tipi e vedrete che il linguaggio si progetterà da sè!"

È 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, 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.