In informatica, un sistema dei tipi è un framework sintattico per la classificazione di espressioni secondo i tipi che esse calcolano.[1] Un sistema dei tipi associa tipi a ogni valore computato. Esaminando il flusso di questi valori, un sistema dei tipi tenta di dimostrare che non avvengano errori di tipo. Il sistema stesso determina che cosa costituisce un errore di tipo, garantendo che le operazioni che si aspettano un certo tipo di valore non siano utilizzate con valori per i quali quell'operazione non ha senso.
La profondità dei vincoli sui tipi e la maniera con cui essi vengono valutati dal sistema influenzano la cosiddetta tipizzazione del linguaggio di programmazione. Nel caso di polimorfismo dei tipi, un linguaggio può associare alla stessa operazione un diverso algoritmo per ogni tipo utilizzabile. Sebbene i sistemi dei tipi concreti utilizzati nei linguaggi di programmazione nascano da problemi di natura pratica di architetture dei calcolatori, implementazione dei compilatori e progetto dei linguaggi, esiste una branca dell'informatica, detta teoria dei tipi, che studia i diversi sistemi dei tipi.
Controllo del tipo
[modifica | modifica wikitesto]Nei linguaggi di programmazione che possiedono un sistema di tipi, il controllo del tipo (in inglese type checking) è l'operazione con cui si determina se il valore assegnato a una variabile sia ammesso per il tipo della variabile. All'interno dei linguaggi tipizzati, si è soliti fare un'ulteriore distinzione tra tipizzazione forte e tipizzazione debole in base alla rigorosità del controllo e alla conversione di tipo implicita. Inoltre, il controllo del tipo può essere statico, se effettuato in compilazione (compile-time) o dinamico, se effettuato durante l'esecuzione (run-time).
Note
[modifica | modifica wikitesto]- ^ Benjamin Pierce, Types and Programming Languages, MIT Press, 2002, ISBN 0-262-16209-1.