Tipizzazione statica

Questa voce o sezione sull'argomento programmazione non cita le fonti necessarie o quelle presenti sono insufficienti.

---

Puoi migliorare questa voce aggiungendo citazioni da fonti attendibili secondo le linee guida sull'uso delle fonti.

Nella teoria dei linguaggi di programmazione, la tipizzazione statica identifica una categoria di sistemi di tipi dove la verifica della compatibilità delle operazioni e l'assegnazione dei tipi a variabili, espressioni e funzioni avvengono già prima dell'esecuzione del programma, generalmente durante la fase di compilazione o tramite strumenti di analisi statica.

Nei linguaggi a tipizzazione statica (come C, C++, Rust, Java e Haskell), il compilatore analizza l'albero della sintassi astratta (AST) confrontando i costrutti del codice sorgente con un insieme di regole logico-matematiche formali. Qualora un'operazione violi i contratti di tipo definiti, il processo di compilazione viene arrestato, impedendo la generazione del codice eseguibile o del bytecode. Questo approccio si contrappone alla tipizzazione dinamica, nella quale i tipi sono associati ai valori a tempo di esecuzione e verificati solo durante l'esecuzione del programma.

Nei linguaggi a tipizzazione statica, gli errori di tipo vengono quindi mostrati durante la compilazione, senza necessità di eseguire il programma. Al contrario, nei linguaggi a tipizzazione dinamica, l’errore di tipo viene rilevato durante l’esecuzione del programma, nel momento in cui viene raggiunta la porzione di codice che lo contiene, causando il sollevamento di un’eccezione.

Fondamenti teorici e operativi

Modelli di esecuzione e layout di memoria

La conoscenza a priori delle strutture dati influenza direttamente il modo in cui il compilatore alloca la memoria e genera il codice macchina:

Nei sistemi a tipizzazione statica:

• I tipi primitivi e le strutture (struct) vengono allocati direttamente sullo stack o in blocchi contigui di memoria heap, senza overhead di metadati.
• L'accesso ai campi di una struttura e la chiamata dei metodi sono risolti tramite offset numerici fissi calcolati a compile-time, traducendosi in istruzioni macchina dirette a basso costo computazionale.

Nei sistemi dinamici, invece, i valori sono memorizzati come oggetti "incapsulati" (boxed objects) o puntatori etichettati (tagged pointers). Un singolo valore scalare richiede un'intestazione contenente puntatori di tipo, contatori di riferimenti e tabelle hash dinamiche, con una conseguente perdita di località spaziale della cache.

Esempi implementativi

template <typename T>
T max_value(T a, T b) {
    return (a > b) ? a : b;
}

int main() {
    int x = 10, y = 20;
    int result = max_value(x, y); // Verificato staticamente; specializzato per interi a costo zero.
    
    // Il seguente codice causa l'arresto della compilazione:
    // max_value(10, "stringa_invalida"); 
    return 0;
}

fn calculate_length(s: &String) -> usize {
    s.len()
}

fn main() {
    let s1 = String::from("hello");
    let len = calculate_length(&s1); // Garanzia statica: s1 è valida e il riferimento è sicuro.
    println!("La lunghezza di '{}' è {}.", s1, len);
}

Inferenza e ricostruzione dei tipi

I moderni linguaggi a tipizzazione statica riducono la verbosità sintattica tramite algoritmi di inferenza dei tipi, che deducono automaticamente il tipo delle espressioni senza richiedere annotazioni manuali esplicite.

L'algoritmo di Hindley-Milner (HM), derivato dal lambda calcolo tipizzato e impiegato in linguaggi funzionali come ML, Haskell e OCaml, garantisce l'inferenza globale del tipo principale (principal type) per ogni espressione ben formata. Si articola in tre fasi:

1. Assegnazione di variabili di tipo: Il compilatore percorre l'AST assegnando variabili di tipo non vincolate () a ogni espressione priva di annotazione.
2. Generazione e unificazione dei vincoli: Mediante l'algoritmo di unificazione di Robinson, il motore risolve il sistema di equazioni di tipo trovando un sostitutore canonico unificato.
3. Let-generalization: Nelle dichiarazioni vincolate (costrutti let), le variabili di tipo libere vengono quantificate universalmente (), originando schemi polimorfici.

Nonostante l'eleganza teorica, HM mostra limiti strutturali nel trattare l'ereditarietà, il subtyping e l'overloading ad-hoc propri della programmazione orientata agli oggetti.

Evidenze empiriche e impatto ingegneristico

Sistemi ibridi: Tipizzazione graduale

Per conciliare la flessibilità dinamica e la robustezza statica è stata introdotta la tipizzazione graduale (gradual typing). Tale paradigma introduce un tipo dinamico incognito (notato come o any) e definisce una relazione di consistenza logica () al posto della stretta equivalenza strutturale.

Ambiti applicativi e criteri di scelta

Voci correlate

• Sistema di tipi
• Tipizzazione dinamica
• Tipizzazione forte
• Tipizzazione debole
• Tipizzazione graduale
• Inferenza dei tipi
• Compilatore
• Analisi statica del software

Bibliografia

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, ISBN 0-262-16209-1.
• Luca Cardelli, Type Systems, in The Computer Science and Engineering Handbook, CRC Press, 1997.
• Siek, Jeremy G.; Taha, Walid, Gradual Typing for Functional Languages, in Scheme and Functional Programming Workshop, 2006.
• Gao, Zheng; Bird, Christian; Barr, Earl T., To type or not to type: quantifying detectable bugs in JavaScript, in ICSE '17: Proceedings of the 39th International Conference on Software Engineering, 2017, pp. 758–769.

Voci correlate

• Tipizzazione dinamica
• Tipizzazione forte

Portale Informatica: accedi alle voci di Wikipedia che trattano di informatica