Per comprendere questa affermazione, dobbiamo prima capire che cosa un sistema di tipo statico ci compra. In sostanza, ciò che un sistema di tipo statico ci dà è una garanzia: iff i controlli del tipo di programma, una certa classe di comportamenti di runtime non può verificarsi.
Sembra strano. Bene, un controllo di tipo è simile a un correttore di teoremi. (In realtà, secondo l'Isomorphism di Curry-Howard, sono la stessa cosa.) Una cosa che è molto peculiare dei teoremi è che quando si dimostra un teorema, si dimostra esattamente quello che dice il teorema, non di più. (Questo è per esempio, perché, quando qualcuno dice "Ho provato questo programma corretto", dovresti sempre chiedere "per favore definisci 'corretto'".) Lo stesso vale per i sistemi di tipi. Quando diciamo "un programma è sicuro dal tipo", ciò che intendiamo è non che non si può verificare alcun errore possibile. Possiamo solo dire che gli errori che il sistema di tipi ci promette di impedire non possono verificarsi.
Quindi, i programmi possono avere infiniti comportamenti di runtime diversi. Di quelli, infinitamente molti sono utili, ma anche infinitamente molti sono "errati" (per varie definizioni di "correttezza"). Un sistema di tipo statico ci consente di dimostrare che non può verificarsi un determinato insieme limitato di infiniti comportamenti runtime non corretti.
La differenza tra i diversi sistemi di tipi è fondamentalmente in cui, quanti e quanto complessi comportamenti di runtime possono dimostrare di non verificarsi. I sistemi di tipo debole come quelli di Java possono solo provare cose molto semplici. Ad esempio, Java può dimostrare che un metodo digitato come restituire String
non può restituire List
. Ad esempio, può non dimostrare che il metodo non verrà restituito. Inoltre, non può dimostrare che il metodo non genererà un'eccezione. E non può dimostrare che non restituirà sbagliato String
- qualsiasi String
soddisferà il controllo di tipo. (E, naturalmente, anche null
lo soddisferà.) Ci sono anche cose molto semplici che Java non può dimostrare, ed è per questo che abbiamo eccezioni come ArrayStoreException
, ClassCastException
, o il preferito da tutti, la% % co_de.
I sistemi di tipi più potenti come Agda possono anche provare cose come "restituirà la somma dei due argomenti" o "restituisce la versione ordinata della lista passata come argomento".
Ora, ciò che i progettisti di Elm intendono con l'affermazione di non avere eccezioni di runtime è che il sistema di tipi di Elm può provare l'assenza di (una porzione significativa di) comportamenti di runtime che in altre lingue possono non essere provato che non si verifichi e quindi potrebbe portare a comportamenti errati in fase di esecuzione (che nel migliore dei casi significa un'eccezione, nel peggiore dei casi significa un arresto anomalo, e nel peggiore dei casi significa nessun arresto anomalo, nessuna eccezione, e solo un risultato silenziosamente sbagliato).
Quindi, non dicono "non implementiamo eccezioni". Stanno dicendo "cose che sarebbero eccezioni di runtime in linguaggi tipici che i programmatori tipici di Elm dovrebbero avere, vengono catturati dal sistema di tipi". Ovviamente, qualcuno proveniente da Idris, Agda, Guru, Epigram, Isabelle / HOL, Coq o lingue simili vedrà Elm come piuttosto debole in confronto. L'istruzione è più indirizzata ai tipici programmatori Java, C♯, C ++, Objective-C, PHP, ECMAScript, Python, Ruby, Perl, ...