Ciao, e benvenuto nella settima puntata della sessantottesima stagione. Nelle due puntate scorse abbiamo visto i modi in cui un'esecuzione può andare male: incastrarsi dove le regole tacciono, o sbandare dove le regole lasciano scegliere. Oggi parliamo di uno strumento che serve proprio a evitare uno di quei disastri, prima ancora di eseguire il programma. Parliamo dei tipi, e della promessa che sanno mantenere.
Partiamo da cosa abbiamo chiamato stallo. Ricordi: un programma si incastra quando arriva in una situazione senza uscita, dove nessuna regola dice come proseguire. Trattare un testo come un numero, chiamare qualcosa che non è una funzione, chiedere un pezzo che non c'è: sono tutti vicoli ciechi dell'esecuzione. E la domanda che ogni progettista di linguaggi si pone è: si può fare qualcosa per impedire che il programma finisca in quei vicoli, senza doverlo eseguire per scoprirlo? La risposta più elegante è il sistema di tipi.
Vediamo l'idea, perché è più profonda di un semplice controllo. Un tipo è, in fondo, una promessa sulla natura di una cosa: questo è un numero, questa è una lista di testi, questa è una funzione che prende un intero e ne restituisce un altro numero. Il controllo dei tipi prende il tuo programma e, senza eseguirlo, verifica che tutte queste promesse siano coerenti: che tu non stia mai per usare un testo dove serve un numero, o per chiamare come funzione qualcosa che non lo è. È un'analisi fatta a tavolino, sul testo del programma, prima che parta un solo passo: si guardano le forme delle cose, non i loro valori concreti.
Nota il legame stretto con la semantica, perché è il cuore della puntata. Il controllo dei tipi è, in sostanza, una previsione. Ragionando sul testo, prevede quali situazioni di stallo il programma potrebbe incontrare eseguendo, e le vieta in anticipo. Non simula ogni esecuzione possibile: usa le promesse dei tipi per dimostrare, con certezza, che certe categorie di vicoli ciechi non potranno mai presentarsi. È un'approssimazione cauta della semantica: guarda al comportamento futuro e ne esclude una fetta pericolosa.
E qui arriva la promessa, quella con un nome quasi solenne. Un linguaggio con un buon sistema di tipi garantisce una cosa precisa: i programmi ben tipati non si incastrano. Se il tuo programma supera il controllo dei tipi, hai la garanzia che, eseguendolo, non finirà mai in uno di quei vicoli ciechi che i tipi sorvegliano. Non è una speranza, è un teorema: qualcuno ha dimostrato, una volta per tutte, che rispettando quelle regole quel disastro non può accadere. Fai bene i conti con i tipi, e un'intera famiglia di errori a runtime sparisce: non perché sei stato fortunato, ma perché era impossibile in partenza.
Voglio farti intravedere come si dimostra una promessa del genere, senza formule, perché è bellissimo. Si regge su due garanzie che lavorano insieme. La prima: da un programma ben tipato, se non è già finito, si può sempre fare almeno un passo. Non ci si può incastrare. La seconda: dopo aver fatto quel passo, il programma è ancora ben tipato, i conti tornano ancora. Mettile insieme e ottieni una catena infrangibile: parti in regola, fai un passo e resti in regola, fai un altro passo e resti in regola, per sempre. Non c'è nessun momento in cui puoi cadere nel vicolo cieco, perché a ogni passo la garanzia si rinnova, come un testimone di correttezza che passa intatto da uno stato al successivo.
C'è un'eco potente della stagione scorsa qui. Parlavamo dei tipi come di un contratto, di un maestro severo che ti corregge mentre scrivi. Era vero, ed era il lato pratico. Oggi vedi il lato profondo: quel contratto è una promessa sulla semantica, sull'esecuzione futura del programma. Il regolamento dei tipi è una regola preventiva, scritta nel gioco per garantire che la partita non si blocchi mai in modo assurdo. Un controllo alla porta che, guardando la forma del programma, esclude in anticipo le partite destinate al vicolo cieco. I tipi non ti correggono solo lo stile: ti proteggono da un pezzo preciso e dimostrabile del futuro.
Resta la lezione di fondo, e va oltre i tipi. Il modo più forte di eliminare un errore non è cercarlo dopo, a caccia nei log: è rendere quell'errore impossibile per costruzione, prima ancora che il programma parta. Un tipo ben scelto trasforma un intero genere di bug da cosa da testare a cosa che non può esistere. Ogni volta che riesci a spostare un controllo dal durante l'esecuzione al prima dell'esecuzione, non stai solo prevenendo un errore: lo stai cancellando dall'insieme delle cose possibili.
Per oggi ci fermiamo qui. Abbiamo visto i tipi non come pignoleria, ma come una promessa sull'esecuzione. Un tipo è una promessa sulla natura di una cosa; il controllo dei tipi, senza eseguire, verifica che quelle promesse siano coerenti, ed è di fatto una previsione: prevede quali stalli il programma potrebbe incontrare e li vieta in anticipo. Da qui la garanzia con un nome quasi solenne: i programmi ben tipati non si incastrano, e non è una speranza ma un teorema. Regge su due garanzie che si rincorrono: da un programma in regola si può sempre fare un passo, e dopo quel passo il programma è ancora in regola. È il lato profondo del contratto di cui parlavamo la scorsa stagione. La lezione: il modo più forte di eliminare un errore è renderlo impossibile per costruzione. Nella prossima puntata: a cosa serve davvero. Nelle note trovi qualche spunto. Se ti è utile, condividila. Grazie per l'ascolto, e ci sentiamo alla prossima.